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}

% 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}