Subversion Repositories TPPL

Rev

Rev 15 | Blame | Compare with Previous | Last modification | View Log | RSS feed

%TODO: disambiguate specification (ML in-out/pre-post) != declaration (thy)
\documentclass[11pt,a4paper]{scrartcl}
 
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage[onehalfspacing]{setspace}
\usepackage{paralist}
\bibliographystyle{alpha}
\usepackage{graphicx}
 
\title{Design and Prototype for a \\
  TP-based Programming Language\\
  {\Large Draft for an FWF proposal}}

\begin{document}
\maketitle
{\small
\begin{spacing}{1}\tableofcontents\end{spacing}
}
\newpage
\section{Scientific aspects}

\subsection{Aims}\label{aims
} %10 pages
This proposal aims at design and development of a prototype
for a programming language, called ``Theorem-Prover based programming
language'' (TP-PL), which

\begin{enumerate}
\item\label{item-comp-func}\textit{adapts the functional programming fragment of
Isabelle}~\footnote{Some details discussed here specifically apply to
the ``High-Order Logic (HOL)'' development of Isabelle.} such that it
becomes appropriate for large software developments in engineering
sciences while exploiting the power of Isabelle's function package and
code generator.
\item\label{item-comp-tools}\textit{accompanies Isabelle's deductive
knowledge with computational tools}, for instance, accompany Isabelle's
Kurzweil-Henstock Gauge Integration in many dimensions with tools to
actually compute integrals; this concerns certified computer algebra.
\item\label{item-comp-interp}\textit{provides an interpreter for the prototyped programming
language} as terms in Isabelle, i.e. in the language layer where
Isabelle tools like simplifiers and tools from computer algebra
(Pt.\ref{item-comp-tools}) reside; the interpreter's design will
extend Isabelle's equational semantics to a big-step operational
semantics.
\end{enumerate
}
TP-PL shall enhance existing tool support for a working engineer as
shown below:
%Fig.\ref{fig-TPPL-survey}:
\begin{spacing}{1}
\begin{figure} [htb]
\begin{center}
\includegraphics[width=100mm]{fig/fig-TPPL-survey-cut
}
%\caption{NEEDS TOO MUCH SPACE}
\end{center}
\label{fig-TPPL-survey}
\end{figure}
\end{spacing}
The present tool support is given by CA systems and CA-based
programming languages. CA shall be enhanced by the above
Pt.\ref{item-comp-tools}, the PL by Pt.\ref{item-comp-func} and the
integration of TP-based CA into the language by
Pt.\ref{item-comp-interp
}. As a by-product, because conceptionally

%TODO vorl"aufige Formatierung
\noindent required by TP-PL, domain knowledge would serve engineers
directly as well.

\medskip
A running example will accompany these sections; the example concerns
a standard problem from a textbook on structural engineering:
%cp from ~/material/texts/emat/lucin/vers1/lucas-interp-100614-KEEPgeom.tex
\medskip %\bigskip ... figure --> other page
\begin{spacing}{1}\label{expl-problem}
\textit{\small Determine the bending line of a beam of length $L$,
which consists of homogeneous material, which is clamped on one side
and which is under constant line load $q_0$; see
Figure~\ref{fig-bend-7-70
}%on p.\pageref{fig-bend-7-70}
% Hint: Use the constraints on the shear force $V(0)=q_0\cdot L$, on the
% bending moment $M_b(L)=0$ and on the expected bending line $y(0)=0$
% and $y^\prime(0)=0$.
%$y(0)=0$, $y^\prime(0)=0$, $V(0)=q_0\cdot L$, $M_b(L)=0$.
.}
\begin{figure} [htb]
\begin{center}
\includegraphics{fig/fig-bend-7-70-en}
\caption{\small\it A balcony under load.}
\end{center}
\label{fig-bend-7-70}
\end{figure}
\end{spacing}
The above mentioned three points will be related to three
respective paragraphs in \S\ref{aims-state}, clarifying the respective
relations to the state-of-the-art. \S\ref{aims-news} will explain how
the project could break new ground scientifically and
\S\ref{aims-results} will estimate the importance of the expected
results for Formal Methods.

\subsubsection{Aims in relation to the state-of-the-art}\label{aims-state}
This section addresses the three aims from p.\pageref{aims} with three
respective paragraphs, eventually cross-referenced by page.

\paragraph{Adapt the functional programming fragment of Isabelle:}\label{aims-state-fun}
Over the years Isabelle has extended it's high-order logic with
a powerful function package and a code generator, such that we can state:
\begin{center}
\textit{Isabelle provides powerful and appropriate prerequisites\\
for the planned programming language, TP-PL ~!}
\end{center}
We just need to adopt Isabelle's existing programming language,
exploit the power of the function package and the code generator and
to extend both mechanisms by modules, featuring larger developments in
engineering applications.

Starting from the running example, the problem stated on
p.\pageref{expl-problem
} can be solved by computations of a program,
which could look like as follows:
% cp from material/texts/present/110731-wroclaw.tex:
\begin{spacing}{1}\label{expl-program}
{\footnotesize\em
\begin{tabbing}
123\=$01$x\=(\=(\=(funs\=(Subproblem (\=\kill
\>$01$  \>{\sc program} bendingLine :: real $\Rightarrow$ real $\Rightarrow$ real (real $\Rightarrow$ real) $\Rightarrow$ bool list\\
\>$02$  \>{\sc program} bendingLine l q v b rb =\\
\>$03$  \>\>({\tt let}\\
\>$04$  \>\>\>(funs::bool list) {\tt =}\\
\>$05$  \>\>\>\>({\sc program} (Bendingline, BeamUnderLoad, Integrate4times) [q, b, v]);\\
\>$06$  \>\>\>(equs::bool list) {\tt =}\\
\>$07$  \>\>\>\>({\sc program} (Bendingline, Constraints, setConstraints) [funs, rb, l]);\\
\>$08$  \>\>\>(sols::bool list) {\tt =} {\sc solve
} equs [$c,c_2,c_3,c_4$];\\
%\>$12$  \>\>\>(sols::bool list) {\tt =}\\
%\>$13$  \>\>\>\>(SubProblem (Real,[linear,equation,system],[])\\
%\>$14$  \>\>\>\>\>[bools equs, reals [c,c\_2,c\_3,c\_4]]);\\
%\>$15$  \>\>\>B {\tt =} {\em Take} ({\tt last} funs);\\
\>$09$  \>\>\>B {\tt =} (({\sc Substitute} sols) {\tt o} ({\sc Simplify} [(bdv, v)] make\_ratpoly\_in)) ({\tt last} funs)\\
%\>$16$  \>\>\>B {\tt =} ((Substitute sols) @@\\
%\>$17$  \>\>\>\>$\;$(Rewrite\_Set\_Inst [(bdv, v)] make\_ratpoly\_in)) B\\
\>$10$  \>\>{\tt in} B)
\end{tabbing}}
\end{spacing}
This program will be referenced subsequently, such hat the essential
features become clear step by step.

\subparagraph{\sc\large Adopt Isabelle's existing programming language:} The
executable fragment of Isabelle consists of data-type and function
definitions.  It's usability even suggests that fragment for
introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
whose type system resembles that of functional programming
languages. Thus there are
\begin{description}
\item[base types,] in particular \textit{bool}, the type of truth
values, \textit{nat}, \textit{int}, \textit{complex}, and the types of
natural, integer and complex numbers respectively in mathematics.
\item[type constructors] allow to define arbitrary types, from
\textit{set}, \textit{list} to advanced data-structures like
\textit{trees}, red-black-trees etc.
\item[function types,] denoted by $\Rightarrow$, will be separately
discussed subsequently.
\item[type variables,] denoted by $^\prime a, ^\prime b$ etc, provide
type polymorphism. Isabelle automatically computes the type of each
variable in a term by use of Hindley-Milner type inference
\cite{pl:hind97,Milner-78}.
\end{description}

\textbf{Terms} are formed as in functional programming by applying
functions to arguments. If $f$ is a function of type
$\tau_1\Rightarrow \tau_2$ and $t$ is a term of type $\tau_1$ then
$f\;t$ is a term of type~$\tau_2$. $t\;::\;\tau$ means that term $t$
has type $\tau$. There are many predefined infix symbols like $+$ and
$\leq$ most of which are overloaded for various types.

HOL also supports some basic constructs from functional programming:
{\it
\begin{tabbing} 123\=\kill
\>$( \; {\tt if} \; b \; {\tt then} \; t_1 \; {\tt else} \; t_2 \;)$\\
\>$( \; {\tt let} \; x=t \; {\tt in} \; u \; )$\\
\>$( \; {\tt case} \; t \; {\tt of} \; {\it pat}_1
  \Rightarrow t_1 \; |\dots| \; {\it pat}_n\Rightarrow t_n \; )$

\end{tabbing} }
\noindent \textit{The running example's program uses some of these elements
(marked by {\tt tt-font} on p.\pageref{expl-program}): ${\tt
let}\dots{\tt in}$
in lines $02 \dots 11$, as well as {\tt last} for
lists and {\tt o} for functional (forward) composition in line
$10$. In fact, the whole program is an Isabelle term with specific
function constants like {\sc program}, {\sc Substitute} and {\sc
Rewrite\_Set\_Inst} in lines $01$ and $10$ respectively.
}

% Terms may also contain $\lambda$-abstractions. For example, $\lambda
% x. \; x$ is the identity function.

\textbf{Formulae} are terms of type \textit{bool}. There are the basic
constants \textit{True} and \textit{False} and the usual logical
connectives (in decreasing order of precedence): $\neg, \land, \lor,
\rightarrow$
.

\textbf{Equality} is available in the form of the infix function $=$ of type $a \Rightarrow a \Rightarrow {\it bool}$. It also works for formulas, where it means ``if and only if''.

\textbf{Quantifiers} are written $\forall x. \; P$ and $\exists x. \;
P$
.  Quantifiers lead to non-executable functions, so functions do not
always correspond to programs, for instance, if comprising \\$(
\;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2
\;)$
.

\subparagraph{\sc\large Exploit the power of Isabelle's function
package} which can generate functional programs from recursive
functions specified in the HOL logic. The power of the package is
indicated by calling an intermediate layer ``Mini-Haskell''
\cite{haftm-nipkow-code-gen-HRS-10}. The package provides specific
support for modeling iteration: In functional programs iteration is
modeled by recursive function calls; this introduces another class of
{\em partiality}, which results from not well-founded recursion and
which might cause non-termination. And termination needs to be proved
in the envisaged context of theorem proving.

However, such termination proofs are gracefully handled by Isabelle's
function package
\cite{krauss:partial06,krauss-fun-def-10}: Given
the definition of a well-known function by \dots

\begin{spacing}{1}
{\small
\begin{tabbing} 123\=$|\;$\=\kill
\>${\it fun}\;{\it fib} :: "{\it nat} \Rightarrow {\it nat}"$\\
\>${\it where}$\\
\> \>$"{\it fib}\;0 = 1"$\\
\>$|$ \> $"{\it fib}\;({\it Suc}\;0) = 1"$\\
\>$|$ \> $"{\it fib}\;({\it Suc}\;({\it Suc}\;n)) = {\it fib}\ n +
{\it fib}\;(S{\it uc}\;n)"$

\end{tabbing}}
\end{spacing}

\noindent\dots Isabelle automatically proves (triggered by
\textit{fun}) termination of this function as well as of nested
recursive and of mutual recursive functions.  The termination prover
\cite{nipkow-krauss:07-find-lex-orders,Krauss:07-size-terminat} is
able to solve termination proof obligations fully automatically,
obviating the need for specifying termination relations. The package
automatically introduces inductive domain predicates which accomplish
several kinds of partiality issues. The termination prover can also
link to external provers and include full proof reconstruction, where
all necessary properties are derived inside Isabelle
\cite{krauss-sternagl-11:terminat-rewrite}.

The function package is not a-priori limited to terminating
recursions, but also works on functions which need not terminate on
all input values. Functions requiring a manual termination proof are
defined by \textit{function} (as opposed to \textit{fun}); users have
the choice of either proving it in terms of the domain predicate, or
specifying a well- founded relation or measure and proving that the
arguments of the recursive calls are decreasing -- which they
typically prefer.

The package automatically provides appropriate proof rules for
reasoning about defined functions and by the way establishes two
appealing advantages: (1) an equational semantics for the programming
language in terms of higher-order rewrite systems
\cite{haftm-nipkow-code-gen-HRS-10} and (2) prerequisites for code
generation, both of which will be re-used in the proposal for
extending the computational tools on p.\pageref{concepts-computation}
and the interpreter of TP-PL. on p.\pageref{concept-interpreter}.

\medskip\textit{The example program on p.\pageref{expl-program}
comprises several such functions: {\sc solve} in line $09$, {\sc
Substitute} and {\sc Simplify} in line $10$ and also {\tt last}, the
latter already defined in Isabelle/HOL.}

\subparagraph{\sc\large Extend the language for large engineering
applications:} The most successful programming languages for applied
mathematics in engineering sciences are based on Computer
Algebra (CA) Systems like \cite{progr-mathematica-2012,prog-maple06
};
in fact, the vast majority of mathematical engineering software is
implemented in those languages.


%TODO PARALLEL ?
%Isabelle now starts to exploit availability of multi-core machines by
%parallel execution which is completely hidden from the user concerned
%with proofs and theory development \cite{parallel-ML}. When designing
%the TP-PL, the question arises how to combine implicit parallelism
%(independent branches of a functional program can be executed in
%parallel) with explicit control of parallel execution by the
%programmer.  \cite{parallel-ML} gives some hints, for instance a
%parallel \textit{map}-function.
%
% The pD Compiler (1993–1994) In my Ph.D. thesis I developed a compiler
% for a small para-functional programming language that used a new
% technique to generate parallelism from annotated functional
% programs. The target code is efficient PACLIB C code with explicit
% task creation and synchronization constructs.
%
% TODO Wolfgang Schreiner ?: pD Compiler ``technique to generate
% parallelism from annotated functional programs''

So, when aiming at a programming language usable for engineers, smooth
integration of CA functionality is indispensable. \cite{plmms10} gives
some ideas. This requirement, however, involves a specific class of
challenges addressed in the second paragraph ``extend Isabelle's
deductive knowledge with computational tools'' on
p.\pageref{concepts-computation}

\medskip The second extension results from the requirement to  assemble a
multitude of functions. The above mentioned function package can
handle functions one by one, so consistent handling of several
functions in one program requires a substantial extension of present
Isabelle. The respective conceptional challenges are addressed in the
third paragraph ``provide an interpreter for the programming
language'' on p.\pageref{concept-interpreter} and respective
technicalities in \S\ref{meth-integrate}.

A particular requirement for large programs is modularisation. Since
TP-PL shall reside within a logical framework, the conception includes
formal specification for programs.

\textit{A specification for particular input data for the running example's
program could be:
}
%Florian's version in Haskell format:
\begin{spacing}{1}\label{expl-spec}
{\small\it
\begin{tabbing}
12345\=12345\=123\=\kill
\>BeamUnderLoad :: (real $\Rightarrow$ real) $\Rightarrow$ real $\Rightarrow$ (real $\Rightarrow$ real)\\
\>BeamUnderLoad $q_0$  L = y\\
\>\>assumes $\;q_0$ is\_integrable $\;\land\;\; L > 0$\\
\>\>yields $y(0) = 0\land y^\prime(0) = 0\:\land\:V(0) = q_0 . L\:\land\;M_b(L) = 0$
\end{tabbing}}
\end{spacing
}
% cp from material/texts/present/110731-wroclaw.tex:
% \begin{spacing}{0.8}\label{expl-spec}
% {\small
% \begin{eqnarray*}
% {\it in} &:& {\it function}\; q_0, {\it length}\; L \\
% {\it pre} &:& q_0\; {\it is\_integrable} \;\land\; L > 0\\
% {\it out} &:& {\it function}\; y(x) \\
% {\it post} &:& y(0) = 0\land y^\prime(0) = 0\:\land\:V(0) = q_0 . L\:\land\;M_b(L) = 0
% \end{eqnarray*}}
% \end{spacing}
\begin{spacing}{1}
{\small
\textit{where $V$ and $M_b$ are constant function symbols in the theory of ``bending lines''. \textit{function} and \textit{length} are functions fixing the arguments' types; $\;q_0$ is a constant function with type $\cal{R} \rightarrow \cal{R}$.}}
\end{spacing}

\bigskip
Sub-programs shall be accompanied by their specifications as well.
There also shall be the possibility to provide several algorithms for
one and the same specification, raising the design question how to
design calls of such subprograms.

\textit{The example program on p.\pageref{expl-program} shows a
preliminary decision for calls of subprograms: these are not called by
their name, but by the keyword {\sc program} followed by a triple: the
theory, the specification and the algorithm.}

\medskip Specifications as well as algorithms shall be assembled in
appropriate data structures in order to facilitate mechanised
search. Definitions, specifications and algorithms are expected to
develop into consistent bodies of domain-specific knowledge order to
improve professionality of development \cite{db:SW-engIII}. For
software engineering such knowledge seems to start~\footnote{In
Isabelle's ``Archive of Formal Proofs'' there are collections like on
``Computer Science $>>$ Security'' with growing lists like ``SIFPL,
VolpanoSmith, HotelKeyCards, RSAPSS, InformationFlowSlicing'', see
http://afp.sourceforge.net/topics.shtml}, also for a few other domains
such knowledge is already mechanised~
\cite{db:dom-eng,Hansen94b,Dehbonei&94}. \cite{plmms10
} describe the
use of such knowledge at a future engineer's workbench.

%TOO SPECIFICL domain knowledge
% The development of such explicit knowledge is already prepared by the
% distinction between the two established notions, quality of design and
% quality of conformance. The former concerns the relation between
% ``reality'' and an abstract model, the latter the relation between the
% abstract model and an implementation. Both relations are increasingly
% investigated and tackled with mathematical methods. One of the
% strongest method is proof; thus one might predict increasing
% importance of mathematical proof in this part software technology.

\paragraph{Accompany Isabelle's deductive knowledge with
computational tools:}\label{concepts-computation} Engineers want
concrete solutions computed for concrete problems like the example
problem on p.\pageref{expl-program}. So this proposal sets the
objective that TP-PL shall shall support calling CA functions, which
in turn set the standards for computational tools.

\textit{In the program for the running example on p.\pageref{expl-program},
the following CA functions are called: {\sc solve} in line $12$ and
{\sc Simplify} in line $14$.}

Since TP-PL is a TP-based language embedded in a logical framework, CA
called by TP-PL needs to integrate into logics. However, mainstream CA
systems, for instance Mathematica and Maple, are weakly founded
(\cite{harr:book} even calls them ``ill-defined'') in terms of
logics. There are various reasons for the mistakes found in mainstream
CA systems: assumptions can be lost, types of expressions can be
forgotten, solutions of an equation have been dropped, etc
\cite{casproto}. So improvements are urgently required, and the
logical foundations of theorem provers like Isabelle are considered an
appropriate prerequisite for such improvements.

\subparagraph{\sc\large Build upon Isabelle's deductive knowledge:}
Isabelle has grown to an extent where application to engineering
sciences (beyond software engineering) comes within reach.  Isabelle's
knowledge developed within HOL primarily addresses topics from
software technology, but also in topics relevant for applied
mathematics the knowledge exceeds what is covered by introductory
courses in engineering studies. Below there is a brief survey of the
knowledge contained in the standard distribution of Isabelle2012~
\footnote{http://http://isabelle.in.tum.de/HOL?TODO} and
in the Archive of Formal
Proofs~\footnote{http://afp.sourceforge.net/topics.shtml}.
\begin{description}\label{isa-know-survey}
\item[Algebra] is developed from groups, rings, fields up to the
fundamental theorem of algebra in the univariate case and Groebner
bases in the multivariate case.
\item[Linear algebra] with executable operations on matrices of
arbitrary dimensions over ordered semirings, elementary linear algebra
on Euclidean spaces, convexity in real vector spaces up to
Gauss-Jordan Elimination for Matrices.
\item[Analysis] includes semicontinuous and continuous functions,
Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality, MacLaurin and
Taylor series, nth roots and the transcendental functions.
\item[Multivariate analysis] concerning Frechet Derivative, Inner
Product Spaces and the Gradient Derivative, Finite-Dimensional Inner
Product Spaces, Multivariate calculus in Euclidean space,
Kurzweil-Henstock Gauge Integration in many dimensions, up to initial
value problems of Ordinary Differential
Equations~\footnote{http://afp.sourceforge.net/entries/Ordinary\_Differential\_Equations.shtml}.
\item[Probability theory] including Binomial Coefficients,
Permutations, Social Choice Theory (Arrow's General Possibility
Theorem, Sen's Liberal Paradox and May's Theorem) and also
Discrete-Time Markov Chains.
\item[Polynomials] in an univariate and in a multivariate version, the
latter addressing monotonicity on strongly normalizing (monotone)
orders.
\item[Number theory] with primality on $\cal N$, congruence, unique
factorization, divisibility in monoids and rings, Residue rings:
Euler's theorem and Wilson's theorem, quotient rings.
\item[Numerals] and their respective arithmetic are all available,
$\cal N, I, Q, R$ and $\cal C$.  For $\cal R$ there are approximations
by floating point numbers~
\footnote{http://isabelle.in.tum.de/dist/library/HOL/Decision\_Procs/Approximation.html}.
\end{description} Following the LCF paradigm all the above knowledge
is derived from first principles, from the axioms of HOL. The axioms,
definitions, theorems and proofs are human readable.

\subparagraph{\sc\large Add CA algorithms based on the deductive
knowledge:} The kind of knowledge as described above, however, is very
different from what applied sciences are used to expect from Computer
Algebra (CA) systems. Isabelle's knowledge is proved mechanically (and
thus reliable), but it does not compute solutions. For instance, the
Isabelle distribution contains this \dots
\begin{spacing}{1}
{\small
\begin{tabbing} 123\=le\=\kill
\>${\it lemma}$\\
\>\>${\it fixes}\;x::"'a::\{{\it idom},{\it number\_ring}\}"$\\
\>\>${\it shows}\;"x^2*y = x^2 \;\&\; x*y^2 = y^2 \longleftrightarrow
x=1 \;\&\; y=1 \;|\; x=0 \;\&\; y=0"$
\\
\>\>${\it by}\;{\it algebra}$
\end{tabbing}}
\end{spacing}
\dots which is not what required: engineers want to have the solution of
equations {\em computed} and not the other way round: find a solution
(somehow -- by hand?) and then let the computer check the correctness.
So, there is a lot to do: computational tools are required to complement
Isabelle's deductive knowledge.

Adding computational tools is essentially more than just copying the
algorithms from CA: CA lacks logical foundations, and the proposed
project is willing not to relax logical rigor established when adding
CA functions. For instance, an equation solver must guarantee to have
found {\em all} solutions to a given equation (system).

Some algorithms already available might not be sufficient engineering
applications.  For instance, Isabelle's development of Gauss-Jordan
elimination~
\footnote{http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml}
states ``Its distinctive feature is succinctness. It is not meant for
large computations.''

\medskip In spite of the challenges mentioned there the proposal is based on the assumption, that implementing a core of CA functions is within reach of
this project:
\begin{compactitem}
\item solving equations in $\cal R$ and $\cal C$
\item solving equational systems in $\cal R$ and $\cal C$, linear and
polynomial
\item univariate and multivariate differentiation and integration
\item some classes of integral and differential equations
\end{compactitem}

\subparagraph{\sc\large Implement CA algorithms using TP-PL:}
As mentioned above,
trustworthiness of CA algorithms requires improvement; such
improvement is addressed by various ways pursued in the domain of TP
as well as in the domain of CA.

This proposal goes it's specific way: it shall improve the
trustworthiness by implementing the CA algorithms by use of the
envisaged TP-PL. This programming language shall have a rigorous
formal semantics embedded into Isabelle's logical framework; this
central issue has already been addressed by paragraph ``adaption of
the programming fragment'' on p.\pageref{aims-state-fun} and will be
elaborated in paragraph ``interpreter for the programming language on
p.\pageref{concept-interpreter
}.

The interpreter of TP-PL to be introduced in the paragraph below will
support interactive program construction --- with respect to CA
algorithms such support will allow for novel ways of exploring the
implemented algorithms. For instance, the shape of the S-polynomial in
the Groebner Bases method for the equational system shown above might
be instructive even for a working engineer (while the hundreds of
rewrites in the same algorithms surely are not).

While the interpreter aims at comprehensibility, transparency and
succinctness, code generation will accomplish efficiency of the code,
including parallel execution.

%DONE 1.1.1.a ---> 1.1.1.b
%The integration entails to
%overcome deficiencies found basically and essentially in CA systems
%and to improve safety and reliability of simplifiers, equation solvers
%and other CA-functionality according to standards of Computer Theorem
%Proving; a specific example is the formalisation of initial value
%problems of
%ODEs~\footnote{http://afp.sourceforge.net/entries/Ordinary\_Differential\_Equations.shtml}.
%The general issue requires specific attention and additional efforts
%described in \S\ref{concepts-computation}.

%probably delete the following paragraph: NO EDUCATION in this proposal!
% \subparagraph{\sc\large Implement advanced algorithms in parallel to elementary}
% algorithms --- this aim continues above-mentioned support for
% transparency: many CA algorithms at the state-of-the-art are
% sophisticated to an extent which is immediately comprehensible only
% for a few experts in the world.
%
% So, in order to make the novel kind of transpacency useful (at least
% with respect to engineering education), in certain cases more
% elementary algorithms might be appropriate and implemented in parallel
% to the advanced algorithms. Of course, being elementary usually trades
% agains generality.

\paragraph{Provide an interpreter for the programming
language:}\label{concept-interpreter} This paragraph explains, how to
bring the ``adapted functional programming fragment of Isabelle''
(first paragraph p.\pageref{aims-state-fun}) with ``extension of
Isabelle's deductive knowledge by computational tools (second
paragraph p.\pageref{concepts-computation}) into effect as a prototype
with some essential features for a future workbench of an engineer.

\subparagraph{\sc\large Support interactive program development} such
that it's complexity can be tackled by a step-wise approach: by
step-wise refinement from abstract to concrete representations,
refinement for all, theories, specifications and algorithms, and
iterating between them, even if all are not complete.

Isabelle/Isar \cite{mw:isar07} supports interactive development well,
also conjoined management of theories and (included) SML
\cite{mak:isar-ml-scala}. So the grounds are laid well for the
proposed extensions. The major extensions are concerned with:
\begin{compactenum}
\item assemblage of a multitude of functions (including their
respective termination proofs) into a program
\item\label{check} check if the pre-conditions of a sub-program can be
derived from the pre/post-conditions of previous (sub-)programs;
prove post-conditions.
\item\label{manag} management of theories, specifications and
programs, which becomes an issue since TP-PL separates these
into three specific collections with prospect to future
enlargements.
\end{compactenum}
Ad Pt.\ref{check}: \textit{For instance, when developing line $09$ in
the running example's program on p.\pageref{expl-program}, one would
be interested if the program's precondition and the preceding
sub-programs' post-conditions can guarantee that {\sc Solve} will
provide a single unique solution for the equational system in
$c,c_1,c_2,c_3$.}

How to adapt Isabelle's mechanisms to accomplish such checks
(\ref{check}.) this question is concern of the next paragraph, how
management (\ref{manag}.) is supported is concern of the subsequent
paragraph.

\subparagraph{\sc\large Extend the interpreter of Isabelle's code
generator:} Isabelle's code generator
\cite{nipkow-bergh-code-gen-02,haftm-nipkow-code-gen-HRS-10} not only
generates code in several languages, but also supports immediate
interpretation of the functions, by use of Isabelle's simplifier
\cite{isa-codegen} and further mechanisms.

Like Isabelle's function package, the code generator only works for
single functions --- so major extensions are required, delving deeply
into Isabelle's concepts and sources, most of which are only
documented by the source code itself. A pleasant exception is
\cite{isar-impl}, which gives some descriptions, for instance of
contexts.

\cite{haftm-nipkow-code-gen-HRS-10} note that ``the code generator
supports stepwise refinement of both algorithms and data by means of
code lemmas that replace less efficient functions and data by more
efficient ones in a uniform and logically sound way'' --- such
stepwise refinement shall remain in focus when tackling design
issues of interactive program development.

\subparagraph{\sc\large Support management of knowledge} as mentioned
in point (\ref{manag}.) above: The algorithms of the selected
exemplary engineering domain shall all be accompanied by rigorous
formal specifications (like the example on p.\pageref{expl-spec}), and
also the CA algorithms to be developed according to paragraph on
p.\pageref{concepts-computation} shall do likewise. Availability of
specifications also enhance usability, because CA algorithms are more
appropriately retrieved by their respective specifications.

So the proposed prototype shall explore possibilities for retrieval of
specifications and algorithms from large bodies of knowledge and for
comparing them: specifications might have relatives (e.g. a type of a
differential equation), one specification might be met by several
algorithms (being comprehensible/sophisticated or fast/slow or just
different), etc.  \cite{plmms10} gives a preview on such choices at a
future engineer's workbench.

Another design challenge is raised by the question how to integrate view on
different language levels: (1) the view on the equations created but
the function package on the level of program code (meta language), and
(2) the view on particular values computed during program
interpretation on the level of program values (object language).

\subparagraph{\sc\large Provide the interpreter with a clear
semantics} which would allow to
\begin{compactenum}
\item step-wise refine data and algorithms
\item step-wise extend a program
\item verify a program (e.g. the example on
p.\pageref{expl-program}) with respect to a specification (e.g. the
example on p.\pageref{expl-spec}).
\end{compactenum}

\textit{In particular, the example's final context on
p.\pageref{expl-ctxt} should allow to prove the example's
post-condition on p.\pageref{expl-spec}}~\footnote{Ideally such proofs
are automated and hidden behind the scenes.}.

Isabelle's function package and code generator, both rely on a shallow
embedding of programs and a semantics in terms of higher-order rewrite
systems \cite{haftm-nipkow-code-gen-HRS-10}. This ``equational
semantics'' has the advantage to reside within Isabelle's inference
mechanisms with the trusted kernel of code.

In case TP-PL suggests to leave this realm of reliability, also for
this case valuable spadework has been done within Isabelle: Jinja
\cite{nipkow-06:java-like} is a complete formal model of a Java-like
language, which includes a formal semantics, type system, virtual
machine model, compiler, and bytecode verifier. The latter has been
re-implemented \cite{imperative-functional-08} based on Haskell's
\cite{jones-haskell-03} imperative specification style where local
state references and mutable arrays can be dynamically
allocated. \S\ref{meth-language
} goes into technical details.

% \subparagraph{\sc\large Regard parallel execution in the semantics:}
% Since several years Isabelle more and more supports parallel execution
% \cite{makarius:isa-scala-jedit} with considerable performance gains
% \cite{Makarius-09:parall-proof}. Hoever, the proof is not yet finally
% established saying that the new mode of execution does not infect the
% system's consistency, in spite of much ongoing work in the field
% \cite{parallel-ML,Wenzel-11:doc-orient,makarius-jEdit-12}.
%
% The envisaged project shall include investigation of parallel
% execution already in the formal semantics, and probably contributes to
% final clarifications for the parallel execution model of the whole
% Isabelle system.

\paragraph{Proof of concept in an exemplary development in an
engineering domain:} The usability of TP-PL shall be tested in a
field-study in cooperation with a selected institute of an engineering
domain (definitely {\em not software} engineering !) at TU Graz.  This
institute is interested in Formal Methods and provides their
students with a comprehensive education in programming.

Students of this institute, which consider a master thesis with a
major mathematical part, shall be invited to accomplish this
mathematics using TP-PL.

The results of their theses are supposed to serve for seminars,
further theses and other educational purposes. The results and
experiences from the field-test are relevant for the respective
engineering domain als well as for the areas of TP and FM.


\subsubsection{How the project breaks new ground
scientifically}\label{aims-news} The project adopts and extends
front-of-the-wave developments extending the computational power of
Isabelle, itself a leading product in the field of deduction and of
mathematics-based, domain-specific knowledge development. The
extension breaks new grounds in several ways:

\paragraph{A novel combination of mechanisms} in Isabelle establishes
novel functionality: the function package
\cite{krauss:partial06,krauss-fun-def-10}, the context mechanisms
\cite{isar-impl} and the machinery of code generation
\cite{nipkow-bergh-code-gen-02,haftm-nipkow-code-gen-HRS-10} are
adapted such that programs can be constructed from several functions,
which can not yet be done. This gives a promising basis for
theoretical work on modularisation mechanisms for larger developments
\cite{TODO-modularisation-togoogle
}.

%extend recently established computational facilities in Isabelle in a
%small but decisive step

\paragraph{Theoretically considered techniques are implemented} first
time: insights gained with MiniMaple \cite{mini-maple-12} serve
logically consistent integration of CA functions and bring
clarification of a rigorous formal semantics
\cite{TODO-semantics-from-others} within reach, which \dots TODO

.\\

\paragraph{Advantages over comparable approaches} seem apparent in the
proposed incremental development in TP-PL with integration of
programming and proving and exploiting refinement techniques
\cite{haftm-nipkow-code-gen-HRS-10}:
\begin{itemize}
\item {\em Advantages in generality} over special purpose languages
like EventML~\cite{eventml-12} \dots TODO \dots
\item {\em Advantages in interactive development} over the work-flow
established for instance in the Focal project~\cite{focal-08}, which
\dots TODO
\item {\em Advantages in integration} over traditional tools in Formal
Methods like the VDM tool box~\cite{vdm-tools-08}, which
\dots TODO
\item {\em Advantages in flexibility and trustability} over
constructive logics like in Agda or in Coq, which integrate deduction
and computation by concept (the Curry-Howard isomorphism) but would
require extension of the trusted kernel by comparable extensions.
\end{itemize}
These advantages are expected to outperform all respective
disadvantages.

\subsubsection{Importance of the expected results for the
discipline}\label{aims-results} The discipline the proposal is
concerned with is Formal Methods (FM) \cite{fm-03}. FM is the approach
to master increasing complexity of technical systems by formal logics:
systems are composed from sub-systems and thus interfaces are crucial,
in particular the properties of dynamic behaviour.

Driven by FM, domain-specific bodies of mechanised knowledge are
emerging, not only for software technology \footnote{For instance, the
Archive of Formal Proofs http://afp.sourceforge.net/} but also for
other engineering domains \cite{db:dom-eng,Hansen94b,Dehbonei&94} and
others.  So-called ``domain engineering'' is expected to create and
mechanise domain specific knowledge \cite{db:SW-engIII},
i.e. appropriate notions (for instance \textit{beam, bending line} in
the running example on p.\pageref{expl}), concise abstractions like
domain specific predicates (for instance \textit{homogeneous, clamped}
in the example) and models, which will develop from kinds of abstract
datatypes to algebraic structures with specific axioms, definitions,
lemmas and theorems. So one might predict increasing importance of
mathematical proof also in these engineering domains.

In spite of increasing demands, FM are still not widely used in
engineering practice.

\medskip\noindent The proposed project intends to promote wider usage
of FM by the following advancements provided by TP-PL:

\begin{compactenum}
\item\textbf{Combination of computation with Formal Methods:}
Programming in the envisaged TP-PL relies on prerequisites from FM and
TP: a specification (in/output, pre/post-condition) must be present,
the notions in the specification must be defined in Isabelle, theorems
used in the program need to be mechanically proved, calling CA
algorithms in the program involves their respective specifications.
Pt.\ref{code-gen} shall ensure that this combination increases
acceptance of FM.
\item\textbf{Dynamic integration of programming and proving} is
particularly supported by the integration of SML code into the logical
infrastructure in Isabelle/Isar. The expected programming environment
of TP-PL will build upon Isabelle's front-end, the plans for extending
this front-end expect prolongation of the front-end's present
usability.

The work-flow envisaged by TP-PL comprises step-wise refinement of
datatypes and algorithms, step-wise completion of programs, proving
pre-conditions automatically or interactively and enhanced usability
in managing large collections of knowledge, in particular the CA
functions.
\item\textbf{Integrated management of large knowledge collections:}
The demonstration study planned for one specific domain is expected
to result in a considerable large collection of knowledge. TP-PL
adds specifications (in/output-items, pre/post-condition) to knowledge
traditionally managed by Isabelle, and TP-PL adds algorithms to knowledge
traditionally managed by FM.

So the project stimulates further research on knowledge management for
specifications and algorithms (which, for instance, are presently not
addressed by the OpenMath
standard~\footnote{http://www.openmath.org/}).
\item\textbf{Verified Computer Algebra} results from the planned
implementation of CA algorithms in TP-PL. The selection of CA algorithms
is related to respective knowledge in Isabelle (about Gr\"obner Bases,
multivariate analysis, etc), which shall be complemented by algorithms
which actually compute solutions.

Of specific importance is the fact, that in this way verified Computer
Algebra is made immediately available for Formal Methods.
\item\label{code-gen}\textbf{Motivation of users by code generation}
has been experienced in several academic courses on FM~\footnote{In
the Isabelle mailing list a thread ``[isabelle] A course based on
Isabelle/HOL and some feedback...''  discusses respective experiences
with http://www.irisa.fr/celtique/genet/ACF/}. TP-PL will extend the
scope of Isabelle's code generator to programs capable of implementing
algorithms solving realistic engineering problems.

So there is the expectation that this kind of motivation will carry
over to the working engineers, such the benefits from automation in
final coding and other advantages will dominate over the hassle with
logical rigor.
\end{compactenum}

The above variety of particular advancements indicates TP-PL's
substantial contribution to the discipline of Formal Methods.  The
integration of all of these features advances over comparable systems
with related features as discussed in \S\ref{aims-news}.


\subsection{Methods
} %4 pages
A review of leading logical frameworks led to the decision for
Isabelle as the conceptional and technological base for prototyping a
programming language in the context of deduction.

Concerning the conceptional base, a principal question is, why the
proposal does {\em not} decide for constructive logics as represented
by Coq~\cite{coq-team-10,coq-logics-93} or
Agda~\cite{agda-wiki,adga-phd-07}. Constructive logics most closely
integrate computation and deduction (due to the Curry-Howard
isomorphism~\cite{TODO-curry-howard}), and this proposal concerns
integration of computation and deduction. The reason is the following:
TP-PL extends computation presently available, and in Coq or Agda such
an extension would affect the core of these systems, enlarge the
amount of trusted code and thus reduce trust in the resulting
programming language.

With the decision for Isabelle in mind, the prototype shall be
developed by different methods with respect to the three aims from
p.\pageref{aims}, described in the first three sections. The forth
section \S\ref{meth-usability} concerns a test of concept for the
prototype.

\subsubsection{Design of language, semantics and
interpreter}\label{meth-language}
This section concerns the work of one PhD. The work starts with
research of the state-of-the-art, the major part is design of novel
software concepts, a modest amount of implementation in included.

\paragraph{Review existing FM tools and programming in TP:}
.\\

Coq, Agda, PVS, ACL2

VDM, B-method, \dots

\paragraph{Extend Isabelle's function package with modules:}
Isabelle provides all prerequisites for a shallow embedding of the
programming language, TP-PL. The implementation of TP-PL
will be a {\em definitional extension} and will introduce all definitions
by reducing it to a simpler form that can be processed by existing
means.  The original specification is then {\em derived} from the
primitive definition by an automated proof procedure. Since all
reasoning is performed within the theorem prover, definitional
extensions are conservative by construction, and thus offer a maximum
of safety.

The requirement for large programs assembling a multitude of functions
raises the need to generalise concepts and code of the function
package.  Large programs also require modularisation. As seen from the
state-of-the-art before the start of the project, it is not clear,
whether this kind of {\em definitional extension} can be maintained
for modularisation, i.e. for programs accompanied with a theory, a
specification (in/output-items, pre/post-condition) and an algorithm.

\paragraph{Research and design a semantics for TP-PL:} As a first
approach to formal semantics for TP-PL we shall take the equaltional
semantics in terms of higher-order rewrite systems. Relating the
equational semantics to an operational semantics for the interpreter
seems simpler than for an imperative language like Java. In case TP-PL
suggests to leave the equational semantics, spadework by
\cite{nipkow-06:java-like} shall be re-used.

The respective virtual machine model will be adapted to capture the
contexts mentioned above together with an environment:

\begin{tabbing} 123\=$|\;$\=\kill
\>${\it type}\;{\it istate} = {\it ctxt}\times{\it env}$
\end{tabbing}

The design of a big-step semantics can re-use many details from
\cite{imperative-functional-08}, for instance the respective
description in relational form as $(h,h^\prime,r) \in [[c]]$ hold iff
the computation $c$ started on heap $h$ does not generate an exception
and yields the result $r$ and the updated heap $h^\prime$. ``Heap''
refers to Haskell's state monad used for imperatively mutable arrays
and adapted as follows:
\begin{spacing}{1
}
%{\small
\begin{tabbing} 123\=$\mathbf{datatype}\;{\it istate}\;{\it
Heap}\;$
\=\kill
\>$\mathbf{datatype}\;{\it istate}\;{\it Heap}$\>$ = {\it Heap}({\it
heap}\Rightarrow({\it istate}+{\it exception})\times{\it heap})$
\\
\>${\it heap}\;f$\>$= {\it Heap}(\lambda h.\;{\it let}\;(x,h^\prime)=
f\;h\;{\it in}\;({\it Inl}\;x,h^\prime))$
\\
\>${\it execute}\;({\it Heap}\;f)$\>$= f$
\end{tabbing
}%}
\end{spacing}

\noindent
Based on this monad big-step semantics is defined as

\begin{tabbing} 123\=$|\;$\=\kill
\>$(h,h^\prime,r) \in [[c]] = (({\it nlf}\;r,h^\prime) = {\it execute}\;c\;h)$
\end{tabbing}

Given this semantics one can prove rules which connect this relation
to the different basic commands. The bytecode verifier is modeled in a
very abstract framework using a semilattice, which hides all the
technical details of the virtual machine. Later, the ``real thing''
can be obtained by instantiation.

The above \textit{istate} in particular will comprise environments
\textit{env$_i$} and (logical) contexts \cite{isar-impl} ctxt$_i$,
which for step-wise interpretation of the example program might look
like on p.\pageref{expl-ctxt} for the running example.

\paragraph{Integrate language and interpreter into Isabelle's code:}
This integration is the major task in the proposed project; so this
task is planned to be done in joint efforts with \S\ref{meth-integrate}.


\subsubsection{Research verification of Computer Algebra and implement
algorithms}\label{meth-ca}
This section concerns the work of a second PhD. The work starts with
researching of the state-of-the-art, combines and integrates concepts
from TP and CA and involves a modest amount of implementation.

\paragraph{Research state-of-the-art in verification of software and CA:}
.\\

FoCal, Axiom, MiniMaple \cite{mini-maple-12}

\paragraph{Review Isabelle's knowledge and select additional CA
algorithms:
}
%TODO redo this paragraph from scratch
Isabelle's deductive knowledge is considered a
sufficient base for developing engineering applications, see
p.\pageref{isa-know-survey}.

However, the only advanced engineering algorithm covered by Isabelle
presently is Fast Fourier Transform over the complex numbers, and its
inverse (using Vandermonde
matrices)~\footnote{http://afp.sourceforge.net/entries/FFT.shtml}.

But even elementary looking CA functions seem not to be trivial: How to
ensure, that no solution is lost in equation solving (in
transcendental equations, in differential equations, etc)~?

\paragraph{Design a structure for related specifications} which at
least occur in a equation solvers: CA systems have, not
explicitly~(!), a hierarchy of types of equations, which are
mechanically searched for matching the input equation until the
appropriate algorithm for solving the equation is found.

TP-PL will have the specifications explicit, and so some kind of
hierarchy will be provided for mechanical search. There are open
questions, for instance how to nicely treat similar equations
(e.q. ``linear equation'') over different domains, integers, reals,
complex numbers and vector spaces.

\paragraph{Distribute implementation in TP-PL to sub-projects:}
The CA functions are implemented using TP-PL. So the respective
sub-projects can start after the interpreter of the TP-PL has
achieved sufficient usability.

The achievement of this usability is the critical point on the
critical path on the time-line to the field-test
\S\ref{meth-usability}.  Thus two teams of students are planned for
years 2/3, one at the institutes for mathematics at TU Graz and one at
RISC Linz.

\subsubsection{Integrate language interpreter and Computer
Algebra}\label{meth-integrate}
This section concerns the work for the Postdoctoral Research Fellow.
The PostDoc must be a former member of the Isabelle developer team,
for the following reasons:

Isabelle is an experimental software with 1.5 Mio LoCs under rapid
development by a team of 5 - 10 PhD and core staff. The code is the
documentation (as usual for well-structured functional code), the
repository provides documentation for dependencies between components
in connection with particular changes in the code. The only reliable
written documentation is \cite{isar-impl}.  Thus becoming able for high
quality contribution to Isabelle code requires several years; so a
novice to Isabelle development would be inefficient in the proposed
project.

\paragraph{Integrate the interpreter into Isabelle:} This integration
requires deeply delving into Isabelle's concepts and sources, for
instance, code generator, contexts, proof state and document model.

In order to give an idea of the interpreter's internal state,
comprising a traditional environment together with logical context,
the following states relate to the program statements in the running
example's program on p.\pageref{expl-program
}:
% cp from material/texts/present/100708-plmms.tex
\begin{spacing}{1}\label{expl-ctxt}
\footnotesize{\it %formulas copied from present/090130-belgrade.tex
\begin{tabbing}
  1234\=$01$xx\=env$_0$ = \{\=ctxt$_0$ $\cup$ 12\=\kill
  \>$01$\>env$_0$ = \{$($l , L$)$, $($ q , $q_0)$, $($ v , x$)$, $($ b , y$\:x)$ ,\\
  \>    \>\>$($rb , $\,[y\:0 = 0\land y^\prime\:0 = 0\:\land\:V\:0 = q_0 . L\:\land\;M_b\:L = 0])$\}
  \\
  \>    \>ctxt$_0$ = \{ $q_0\; {\it is\_integrable\_in}\; x\;,\; L > 0$ \
}
  \\
%_______vvvvvvv
\>$04$\>env$_1$ = env$_0$ $\cup$ \{$($funs , $[V x = c - q_0\cdot x \;, M_b\: x = c_2 + c\cdot x - \frac{q_0}{2}\cdot x^2\;,$\\
\>    \>\>\>$y^\prime\:x = c_3 - \frac{1}{EI}\cdot(c_2 + \frac{c}{2}\cdot x^2 - \frac{q_0}{6}\cdot x^3) \;,$\\
\>    \>\>\>$y\:x = c_4 + c_3\cdot x - \frac{1}{EI}\cdot(\frac{c_2}{2}\cdot x^2 + \frac{c}{6}\cdot x^3 - \frac{q_0}{24}\cdot x^4)]$
\}
\\
\>    \>ctxt$_1$ = ctxt$_0$ $\cup$ \{ $q_0\; {\it is\_integrable\_in}\; x \;,\; y^{\prime\prime}\:x = -\frac{1}{\mathit{EI}}\cdot M_b\:x \;,$\\
\>    \>\>\>$y^{\prime\prime\prime}\:x = -\frac{1}{\mathit{EI}}\cdot V\:x  \;,\; y^{\prime v}\:x =  q_1\:x$ \
}
\\
%_______vvvvvvv
\>$07$\>env$_2$ = env$_1$ $\cup$ \{$($equs , $[L\cdot q_0 = c\;,\; 0=c_2 + 2\cdot L\cdot c - \frac{L^2\cdot q_0}{2}\;,$\\
\>    \>\>\>$0=c_4\;,\; 0=c_3 ])$
\}
\\
\>    \>ctxt$_2$ = ctxt$_1$ $\cup$ \{pre-condition skipped , post-condition skipped\
}
\\
%_______vvvvvvv
%\>$14$\>env$_3$ = env$_2$ $\cup$ \{$($sols , $[c=L\cdot q_0\;,\;c_2=\frac{-L^2\cdot q_0}{2}\;,\; c_3=0\;,\;c_4=0])$\}
%\\
%\>    \>ctxt$_3$ = ctxt$_2$ $\cup$ \{pre-condition skipped , $\forall s\in \mathit{sols}\,.\; \mathit{Substitute}\;\mathit{sols}\;s\}$\\
%_______vvvvvvv
%\>$15$\>env$_4$ = env$_3$ $\cup$ \{$($B , $y\:x = c_4 + c_3\cdot x - \frac{1}{EI}\cdot(\frac{c_2}{2}\cdot x^2 + \frac{c}{6}\cdot x^3 - \frac{q_0}{24}\cdot x^4)$\}\\
%\>    \>ctxt$_4$ = ctxt$_3$ $\cup$ \{\}\\
%_______vvvvvvv
\>$09$\>env$_5$ = env$_4$ $\cup$ \{$($B , $y\:x = (0) + (0)\cdot x - \frac{1}{EI}\cdot(\frac{   \left(\frac{-L^2\cdot q_0}{2}\right)    }{2}\cdot x^2 + $\\
\>    \>\>\>$\frac{   \left(L\cdot q_0\right)   }{6}\cdot x^3 - \frac{q_0}{24}\cdot x^4)$\}
\\
\>    \>ctxt$_5$ = ctxt$_4$ $\cup$ \{\
}\\
%_______vvvvvvv
\>$10$\>env$_6$ = env$_5$ $\cup$ \{$($B , $y\:x= \frac{q_0\cdot L^2}{ 4\cdot{\it EI}}\cdot x^2
                    -\frac{q_0\cdot L  }{ 6\cdot{\it EI}}\cdot x^3
                    +\frac{q_0         }{24\cdot{\it EI}}\cdot x^4)$
\}\\
\>    \>ctxt$_6$ = ctxt$_5$ $\cup$ \{ $\neg(y\:x\;\mathit{contains}\;\{c,c_2,c_3,c_4\})$ \
}%\\
%\\
%\>ctxt$_i$ = env$_i$ $\cup$ ctxt$_i$
\end{tabbing}
}
\end{spacing}
The numbers on the left refer to the numbers in the example program on
p.\pageref{expl-program}.

\paragraph{Supervise integration of CA into Isabelle:}
TODO

\paragraph{Extend Isabelle/jEdit as mini-IDE for TP-PL:} As mentioned,
Isabelle is under rapid development; this is particularly true for the
new front-end based on jEdit running the Java Virtual Machine and thus
opens TP for the world outside Linux, Emacs and single/local processing.

The conception of TP-PL requires some functionality in addition to
present Isabelle/jEdit: programming in TP-PL involves search and
management of collections of specifications and of algorithms. Also
dynamic views of the interpreter state are planned for debugging.

\paragraph{Assist the project leader} in particular with decisions
related to Isabelle's internals and in cooperation with the institute
engaged in the proof of concept according to \S\ref{meth-usability}.

There are also several supervision tasks: assistance for the students
performing the proof of concept (who only can be expected to
accomplish specifying and programming in TP-PL, but not proving
theorems) as well as supervision of thes students engaged in
sub-projects on Computer Algebra according to \S\ref{meth-ca}.


\subsubsection{Proof of concept in an  selected exemplary engineering
science}\label{meth-usability} As soon as the language definition has
been clarified according to \S\ref{meth-language}, topics and problems
for programming can be selected. The selection requires cooperation
with \S\ref{meth-ca}: the CA functions required for programming
solutions for the selected problems must be developed; there might be
constraints on the selection from \S\ref{meth-ca}.

\paragraph{Implement engineering problems in TP-PL:} Implementation is
done at the selected institute. In order to make work efficient, a
team of students shall be gathered, where each individual is working
on his or her thesis independently, by sharing experience with
development in TP-PL.

The implementation work comprises development of definitions and theorems
(with decisive support in proving), of specifications and of
algorithms.

\paragraph{Compile guide lines for TP-PL programmers} is planned as a
by-product of supervising the students working in the proof of
concept. This task requires coordination with all other tasks
\S\ref{meth-language}, \S\ref{meth-ca} and \S\ref{meth-integrate}.


\subsection{Work plan, time plan and dissemination plan
} %1page
\subsection{Cooperations} %1 page
\section{Human resources} %1 page
\subsection{Scientific qualifications of the scientists involved}
\subsection{Importance of the project for the career development}
\section{Potential additional aspects
} %1 page
%\newpage
\subsection{Implications for other branches of science} All sciences'
formal parts are addressed by Formal Methods (FM) in principle, but as
mentioned in \S\ref{aims-results
}, not even the technology oriented
sciences widely use Formal Methods. An adjacent discipline, ``Systems
Modelling'' (SM)), tries to bridge the gap between graphic-oriented
methods (traditionally from UML etc) and more formal methods --- and
also there the former still seem to surpass the latter.

% http://www.springerlink.com/content/109378/
% Software and Systems Modeling
% Volume 1 / 2002 - Volume 11 / 2012
% http://www.sosym.org/ ... editorial !

A most recent advancement on the graphical side are ``System
Modelers'' based on
CA~\footnote{http://www.maplesoft.com/products/maplesim/,
http://www.wolfram.com/system-modeler/}: these provide rendering and
animation such that the engineers' intuition is addressed and
iterations in development can be driven by such intuition.

\medskip However, experiences from FM
demonstrate~\cite{FME-97,FME-96}, that formal rigor surpasses human
intuition the more complex systems become. So what seems urgently
needed is
\begin{center}
{\it FM} + SM = {\it F}SM $\;$ ({\it Formal} Systems Modelling)
\end{center}
i.e. underpinning the toos for SM with formal rigor from FM and TP
such that critical features of systems can be rigorously verified.

By extending computational expressiveness while maintaining logical
rigor, the proposed TP-based programming language might
\textit{supplant a missing link at a crucial point}: the prototype
shall demonstrate potential to gradually substitute CA-based languages
within all the upcoming tools in (F)SM.

\subsection{Effects that will have implications beyond the field} With
respect to the essential role of Formal Methods for reliable systems,
there is hope for effects on the general attitude towards science and
technology.

Such effects are desirable for experts and developers as well as for
the public. The proposed TP-PL specifically addresses engineers and
will first be applied in engineering science education according to
\S\ref{aims}.  Cost reduction by FM in development of complex systems
is widely acknowledged.

TP-PL is in company with development of formal domain knowledge as
shown in \S\ref{aims-results}. Such domain knowledge is developed {\em
preceeding} actual development of systems, crucial systems'
features become evident early and widespread adoption of FM in technology
standards is desirable.

All this enables the public for earlier involvement in technology impact
assessment --- and the project consortium hopes that TP-PL can provide
a right kick at a right point at the right time.

\section{Financial aspects
} %1 page
\subsection{Information on the research institution}
%- available personnel not financed by the FWF (usually the project
%  leader and co-applicants);
%- available infrastructure:

\subsection{Information on the support requested}
%- concise justification for the personnel requested (type of
%  position(s), description of nature of work, length and extent of
%  involvement in the project)
%- concise justification for the non-personnel costs (equipment,
%  material, travel and other costs). If equipment is requested,
%  applicants must specify why this does not represent part of the
%  available infrastructure (see also Appendix 2.3).

\section{CVs and publication lists}
\subsection{Wolfgang Schreiner}
\subsection{Franz Winkler}
\subsection{Amine Chaieb}


\begin{spacing}{1}\bibliography{references}\end{spacing}

\end{document
}