Subversion Repositories TPPL

\subsection{Specification and proof language Isar}

\subsection{Specification and proof language Isar}\label{Isar}

    systems using code generation \refme.

    systems using code generation \secref{code-generation}.

%%% code generation, datatype refinement and reflection, embedded

it is possible to generate code from specifications and run that code

%programming language %% making things executable

in its target language environment.  Isabelle implements code generation

% \cite{haftm-nipkow-code-gen-HRS-10}

by turning a suitable set of equational theorems into a program

% The executable fragment of Isabelle together with the function

with the \emph{same equational semantics} in a specific language; currently,

% package and with the code generator provide a promising basis for

Standard ML, OCaml, Haskell and Scala are supported

% prototyping such a language, more supportive and more reliable than

\cite{haftm-nipkow-code-gen-HRS-10}.  Typical applications of code generation

% a CA-based one.

\begin{itemize}

% \item\label{item-comp-func}\textit{adapts the functional programming

  \item Turning a specification into a executable program which

% fragment of Isabelle}~\footnote{Some details discussed here

  \item Using generated code as a fast evaluator.  This is

% specifically apply to the ``High-Order Logic (HOL)'' development

    particularly suitable for decision procedures, i.e.~

% of Isabelle.} such that it becomes appropriate for large software

    procedures that solve a class of problems programmatically

% developments in engineering sciences while exploiting the power of

    but by construction of a suitable proofs, which often involves

% Isabelle's function package and code generator.

    heavy equational rewriting \cite{Chaieb-PhD}.

% \subparagraph{\sc\large Extend the interpreter of

\end{itemize}

% Isabelle's code generator:} Isabelle's code generator

A particularity of Isabelle's code generator is that it comes

% not only generates code in several languages, but also supports

with support for algorithm and datatype refinement, which allows

% immediate interpretation of the functions, by use of Isabelle's

it e.g. to implement (finite) sets by balanced trees in a trustable way (see

% simplifier \cite{isa-codegen} and further mechanisms.

\cite{isa-codegen}) – and thus more performant code.

% Like Isabelle's function package, the code generator only works

Note that specifications restricting themselves to the shallowly

% for single functions --- so major extensions are required, delving

embedded programming language of Isabelle identified in \secref{Isar}

% deeply into Isabelle's concepts and sources, most of which are

can (almost) always be turned into programs by code generation

% only documented by the source code itself. A pleasant exception

without further ado, which enables engineers etc. developing

% is \cite{isar-impl}, which gives some descriptions, for instance

algorithms in them are able to see their algorithms work on

% of contexts.

other platforms, too.

% \cite{haftm-nipkow-code-gen-HRS-10} note that ``the code generator

For specifications which go beyond that language, there is still

% supports stepwise refinement of both algorithms and data by means

a high chance that reasonable subsets can be turned executable

% of code lemmas that replace less efficient functions and data by

by providing reasonable models for the involved types. E.g.~although

% more efficient ones in a uniform and logically sound way'' ---

rational numbers in Isabelle are constructed abstractly using

% such stepwise refinement shall remain in focus when tackling design

quotients, they are executable by default since at the same

% issues of interactive program development.

time an implementation by pairs of integer numbers is provided.