Subversion Repositories TPPL


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

% text max. 450 words

\textheight = 26cm %24 cm still show the page no.
\textwidth = 15cm

FWF Proposal

\noindent\hspace{.57cm}\textbf{\Large Design and Prototype for}

\noindent\hspace{.4cm}\textbf{\Large a TP-based Programming Language}

\bigskip\textit{This proposal concerns the question about how (Computer)
Theorem Proving (TP) can provide tool support for an engineer working
at a future virtual workbench.}

\bigskip Engineers are used to have tool support from Computer Algebra
(CA) and from programming languages (PL). In order to prepare for
viable transitions into the future, this proposal concerns
an indirect way via adaption of existing tools, via CA and via PL.

\medskip CA provides powerful tools for computing
concrete results with respect to concrete problems. Specific
PL, in turn, provide a general tool for combining CA
algorithms with programs which compute such results for such
problems. Consequently, the vast majority of engineering software is
implemented by \textit{CA-based programming languages}.

\medskip Since technical systems have become and more more complex,
Formal Methods (FM) helped to master complexity by rigorous formal
specification of the systems and by proof of crucial system's
features. However, FM are still not widely used in engineering
practice, apparently tool support for integration of formality and
practice still needs improvement.

\medskip Herewith, in cooperation between RISC Linz and TP Group
Munich prototyping such integrated tool support is proposed.  The
proposal is based on Munich's TP Isabelle and extends the existing
tool support on three ways:
\item\textit{Provide a logical base for CA algorithms} which are not
yet formally specified and which still struggle with inconsistencies,
for instance with ``multivalued'' functions. TP is appropriate for
handling logical assertions during computation of such functions and
more generally, for specifying and verifying algorithms.
\item\textit{Prototype a TP-based programming language} which reliably
calls CA algorithms, specified and verified. The executable fragment
of Isabelle together with the function package and with the code
generator provide a promising basis for prototyping such a language,
more supportive and more reliable than a CA-based one.
\item\textit{Implement domain-specific knowledge
} for an exemplary
selected engineering domain (software engineering excluded!). Such
knowledge formalises notions, for instance in structural engineering
``beam'', ``frame-work'' or ``load''. Such prepared notions serve the
engineer and support reliability of his or her design activities.
%constitute accurate specifications and guard the calls of CA.

\medskip The core of the proposal is the TP-based programming language:
programs written in this language build upon specifications developed
within the domain-specific knowledge, call verified CA algorithms,
guard the calls with specifications and thus compute concrete results
more trustably.

\medskip So TP-based languages promise to decisively act as
a missing link between the offers of FM and the factual needs of
working engineers in the future.
% Vienna Development Method, the cradle of FM, this project ...
% More exotic features: In earlier versions of the VDM-SL tools there
% was also support for parameterized modules and instantiations of such
% modules. However, these features was taken out of VDMTools around 2000
% because they was hardly ever used in industrial applications and there
% was a substantial number of tool challenges with these features.
% ... what about ML modules ?
% Functional Modelling + State-based Modelling
% ...Each step of refinement involves Data Reification, then Operation
% Decomposition...