Subversion Repositories TPPL

Rev

Blame | Last modification | View Log | RSS feed

% outdated version kept for simple copies
% outdated version kept for simple copies
% outdated version kept for simple copies

% aims:
% * support for agreements in project planning:
%   * What is the TPPL prototype good for ?
%   * What are general directions of development for successors ?
%   * Reflect possibly different views of TP, software verification and CA
% * raw material for proposal


\section*{---------------}
This is another text (in line with the ``statement why Isabelle/HOL is
the system of choice'' and ``Theorem Proving underway to Engineering
Practice'') preparing for a project with the tentative title ``Design
and Prototype for a TP-based Programming Language'' and preparing for
cooperation between the Theorem Proving Group Munich and RISC Linz.

\section{Requirements from joining computation and
deduction}\label{requirements}
This is a kind of protocol while approaching Isabelle from the side of
CA and from the side of Formal Methods (FM), too. These sides
emphasise a computational point of view combined with decisive
interest in software verification. Furthermore, general views on the
relation between ``Computation'' and ``Deduction'' have been developed
at RISC, which come into consideration as well. The goal of this
``protocol'' is to serve detailed project planning in cooperation
between Munich and Linz.

Above all, the proposal's approach aims at a practicable solution,
which uses Isabelle as carrier for a shallowly embedded functional
programming language. ``Shallow'' means, that any extension shall be
conservative with respect to trustability established by Isabelle.
``Practicable'' means, that the approach intends to re-use as much of
tools and code existing in Isabelle, including the front-end
Isabelle/jEdit.

\subsection{Requirements for computation arising step by
step}\label{req-steps}
Approaching from the side of computation, the extent of Isabelle's
support for functional programming comes as a surprise: support for
proving termination \cite{krauss-fun-def-10}, for datatypes and for
code generation \cite{isa-codegen}, naturally embedded into Isabelle's
deductive framework and respective proof tools.

Isabelle's existing features for programming motivate visions which
immediately go beyond the state-of-the-art in several directions
described in the sequel.

\begin{enumerate}
\item\label{spec}\textbf{Extend functions with preconditions to
``programs'':} Given an example, a specification which involves a
precondition:
\label{gcd_poly}
{\small
\begin{verbatim}
locale gcd_poly =
  fixes gcd_poly :: int poly -> int poly -> int poly
  assumes gcd_poly a b = c
    and not (a = [:0:])
    and not (b = [:0:])
    ==> c dvd a and c dvd b
      and forall c'. (c' dvd a  and  c' dvd b) => c' =< c
\end{verbatim}
}%\small
Computation of a function's value is considered meaningless for input
values not meeting the preconditions. In the above example computation
of the \texttt{gcd} is meaningless for zero polynomials, i.e. for
\texttt{a = [:0:]} and \texttt{b = [:0:]}.

While High Order Logic (HOL) takes all functions as total functions
and this way allows for elegant and short proofs (for instance, that
some code implementating the above specification meets the
postcondition \texttt{ c dvd a and c dvd b and forall c'. (c' dvd a
and c' dvd b) => c dvd c'}, practice of programming hardly can agree
with computations which lead to an ``undefined'' value or to
non-termination.

So our approach suggests to execute functions only after a positive
check of preconditions. To this end, one could introduce the notion of
``program'' (or ``method''?): {\em a program is a function guarded by
a specification.}

\item\label{subprog}\textbf{Combine programs to larger programs:}
Once guarded programs are introduced, there is the requirement to
combine programs (probably retrieved from some library) to larger
programs.

While assembling such programs from statements, from functions and
from other programs, requests for proving appear: a call for a guarded
subprogram requires checking the guard --- this involves proving the
respective precondition from the initial precondition (of the main
program), from lemmas about previous functions and from postconditions
of previous programs.

\fixme[discuss Isabelle tools for preconditions with Florian] TODO: We
can not yet imagine the details of combined handling of programming
and proving within Isabelle's existing tools.  \S\ref{req-combine}
below comes back to this open question from another side in
Pt.\ref{item-combine-Isa-code}.

\item\label{item-interp}\textbf{Model dynamic progression in computation:} Construction
of a program from subprogram to subprogram as described in
Pt.\ref{subprog} above, requires to build a logical context from
preconditions and postconditions alongside the progression of program
development.

This kind of progression is related to a dynamic view, as opposed to
the static view of Isabelle/Isar proof documents --- a view which is
highly valuable in the theory of programming. However, the practice of
programming generally relies on dynamic views alongside the
interpretation of programs.

\medskip Modeling of dynamic progression in computation is not only
required according to Pt.\ref{subprog} above, but also in implementing
logically valid CA. For instance, simplifying a term which contains
so-called ``multivalued functions'' ($\sqrt{\;\;\;}, \tan^{-1}$, etc)
is an important unresolved question in
CA~\cite{davenport-10:multivalued}.  The unresolved problem are case
distinctions recurring at each such function, dependent on predicates
from previous occurrences of other such functions. Our approach plans
to tackle this problem by TP technology called from within CA
algorithms. These calls arise at each occurrence of such a function,
with predicates of increasing complexity during
interpretation. \fixme[Wolfgang, please, better explanation?, better
example for multivalued functions?
]

Isabelle/Isar already implements a mechanism modelling dynamic
progression during interactive construction of Isar proof documents.
To integrate some kind of program interpreter into existing mechanisms
in Isabelle is a particular challenge for our
approach. \fixme[Florian, please, comment on this.]

\end{enumerate}

\subsection{Mutual dependencies between deduction and
computation}\label{req-combine}
While the previous \S\ref{req-steps} step-wise followed motivations
towards integration of computation and deduction, this section goes
into technical details on an abstract level. This abstract level shall
be refined to a concrete proposal (section ``Methods'', \S{1.2} in the
proposal); \S\ref{req-tools} will provide prelimianry notes on that.

\begin{enumerate}
\item\label{item-combine-Isa-code}\textbf{Mutual dependencies between
Isabelle and generated code:} Given Isabelle's function package, proof
tools and code generator, the planned approach suggests to investigate
the following cases:
  \begin{enumerate}
  \item\textbf{Full embedding into Isabelle} is already realised
and usable for functions without guards: functions can be defined,
respective properties (in particular postconditions like \texttt{ c
dvd a and c dvd b and forall c'. (c' dvd a and c' dvd b) => c dvd c' }
on p.\pageref{gcd_poly} above) can be proven and the functions can be
evaluated by \texttt{value} --- all within Isabelle.

  \item\textbf{Stand-alone generated code} is already realised and
usable for functions without guards: Given a combination of functions
like \texttt{gcd\_poly}, where the respective preconditions all can be
checked by generated code, like \texttt{a = [:0:]} and \texttt{b =
[:0:]} in the example --- then the generated code runs stand-alone
from Isabelle (while every rewrite step performed by the program can
be simulated in the logic, which guarantees partial correctness
\cite{haftm-nipkow-code-gen-HRS-10}).

  \item\textbf{Calling TP mechanisms from generated code,} however,
becomes necessary, as soon as a precondition cannot easily be
expressed in the logic of the target language of code generation. This
approach plans to involve preconditions like \texttt{f
is\_differentiable\_on M}, which are straight forward in Isabelle's
rich logic, but not in the targeted programming languages.

  \item\textbf{Integration of generated code in Isabelle} is the other
way round: For instance, code generated from an implementation of
\texttt{gcd\_poly} is much more efficient that \texttt{value} using
the simplifier. So more or less dynamic embedding of generated code
needs to be considered with respect to more or less dynamic program
development in Isabelle.

  \end{enumerate} Consideration of these four cases will have impact
on an Isabelle ``program development environment'' as motivated in
\S\ref{req-steps}.
\item\textbf{Hierarchies of specifications} will be required for
implementation of verified CA. For instance, the Risch
Algorithm~\cite{Geddes-92:comp-alg} decomposes the general problem of
integration to methods for integrating rational functions, radicals,
logarithms, and exponential functions. This approach plans to guard
each of these methods (``programs'') with a specification and to
assemble all specifications in a tree.

Certain branches of that tree will address integration, other branches
will address equation solving for algebraic, differential and integral
equations, etc. There are ideas about automated ``problem refinement''
by searches along branches. \fixme[Wolfgang, please, better
explanation?, better example for hierarchies of types of equations,
etc?
]

\medskip These plans suggest to pay further attention to
specifications introduced in \S\ref{req-steps} Pt.\ref{spec}:
specifications play an important role in modeling partial functions,
specifications contribute to proving properties of programs
(Pt.\ref{subprog} in \S\ref{req-steps}) and specifications guard the
interpretation of functions in various ways
(Pt.\ref{item-combine-Isa-code} in \S\ref{req-combine}), and there
might be further roles.

\item\textbf{TODO}
\end{enumerate}

\subsection{Programming tools derived from Isabelle's
features}\label{req-tools}
In order to focus efforts on creating novel features, this proposal
plans to adopt Isabelle's concepts as they are, and it is interested
to re-use existing code as much as possible.  \fixme[Florian, please,
help to indentify code to be re-used as much as possible
]

\bigskip TODO this section particularly calls for discussions and
refinement towards a proposal.

\begin{enumerate}
\item\textbf{TODO}

\item\textbf{TODO:} How to represent combinations of functions and
programs for convenient handling according to \S\ref{req-steps}
Pt.\ref{subprog}?  Represent by an Isabelle term, re-using many of
Isabelle's features for parsing, pretty printing, etc?

\item\textbf{TODO:} How support interactive programming / proving
in accordance to \S\ref{req-steps} Pt.\ref{item-interp}? Contexts?

\item\textbf{Tools for debugging:} Assuming a design decision for
modeling combinations of subprograms (cf. \S\ref{req-steps}
Pt.\ref{item-interp}) by Isabelle terms, the jEdit user
interface~\cite{Wenzel-11:doc-orient
} promises much of functionality
of state-of-the-art debuggers without much further ado: The access to
underlying data of several kinds via tool-tips is already there.

% \item\textbf{}
%   \begin{enumerate}
%   \item\textbf{}
%   \item\textbf{}
%   \item\textbf{}
%   \end{enumerate}

\item\textbf{TODO}
\end{enumerate
}