# Subversion RepositoriesTPPL

Rev
Rev 37 Rev 39
Line 102... Line 102...
102
Isabelle also comes with syntactic sugar for \emph{if}-, \emph{let}- and

102
Isabelle also comes with syntactic sugar for \emph{if}-, \emph{let}- and

103
\emph{case}-expressions known from functional programming, which are

103
\emph{case}-expressions known from functional programming, which are

104
internally mapped to suitable combinators.

104
internally mapped to suitable combinators.

105


105


106


106


107
\subsection{Specification and proof language Isar}

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

108


108


109
To conduct formal developments, Isabelle uses the specification

109
To conduct formal developments, Isabelle uses the specification

110
and proof language \emph{Isar}.  An Isar text is

110
and proof language \emph{Isar}.  An Isar text is

111
structured as a series of Isar commands, each consisting of a

111
structured as a series of Isar commands, each consisting of a

112
particular keyword followed by text denoting logical and non-logical

112
particular keyword followed by text denoting logical and non-logical

Line 163... Line 163...
163
  \item Algorithmic issues can be expressed directly in a functional style

163
  \item Algorithmic issues can be expressed directly in a functional style

164
    in Isabelle, which eases transfer of algorithms from CA to Isabelle.

164
    in Isabelle, which eases transfer of algorithms from CA to Isabelle.

165


165


166
  \item Formulations in the embedded functional programming language

166
  \item Formulations in the embedded functional programming language

167
    can be translated to code for common functional programming language

167
    can be translated to code for common functional programming language

168
    systems using code generation \refme.

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

169


169


170
\end{itemize}

170
\end{itemize}

171


171


172
\fixme[elaborate: comparison to other systems]

172
\fixme[elaborate: comparison to other systems]

173


173


Line 364... Line 364...
364
apart from similar systems in that respect.

364
apart from similar systems in that respect.

365


365


366


366


367
\subsection{Code generation and datatype refinement}\label{code-generation}

367
\subsection{Code generation and datatype refinement}\label{code-generation}

368
368


-

369
To avoid the overhead of computations \emph{within} the proof assistant,

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

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

370
%programming language %% making things executable

371
in its target language environment.  Isabelle implements code generation

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

372
by turning a suitable set of equational theorems into a program

372
-

373
% The executable fragment of Isabelle together with the function

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

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

374
Standard ML, OCaml, Haskell and Scala are supported

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

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

-

376
are:

-

377


376
% a CA-based one.

378
\begin{itemize}

377
379


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

380
  \item Turning a specification into a executable program which

-

381
    by construction obeys the original specification.

-

382


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

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

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

384
    particularly suitable for decision procedures, i.e.~

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

385
    procedures that solve a class of problems programmatically

382
% developments in engineering sciences while exploiting the power of

386
    but by construction of a suitable proofs, which often involves

383
% Isabelle's function package and code generator.

387
    heavy equational rewriting \cite{Chaieb-PhD}.

384
388


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

389
\end{itemize}

-

390


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

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

387
% \cite{nipkow-bergh-code-gen-02,haftm-nipkow-code-gen-HRS-10}

-

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

392
with support for algorithm and datatype refinement, which allows

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

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

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

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

391
395


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

396
Note that specifications restricting themselves to the shallowly

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

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

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

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

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

399
without further ado, which enables engineers etc. developing

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

400
algorithms in them are able to see their algorithms work on

397
% of contexts.

401
other platforms, too.

398
402


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

403
For specifications which go beyond that language, there is still

400
% supports stepwise refinement of both algorithms and data by means

404
a high chance that reasonable subsets can be turned executable

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

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

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

406
rational numbers in Isabelle are constructed abstractly using

403
% such stepwise refinement shall remain in focus when tackling design

407
quotients, they are executable by default since at the same

404
% issues of interactive program development.

408
time an implementation by pairs of integer numbers is provided.

405
409


406
410


407
\subsection{Integration of external tools}\label{external}

411
\subsection{Integration of external tools}\label{external}

408


412


409
Over the years, various external tools have been hooked to the Isabelle

413
Over the years, various external tools have been hooked to the Isabelle

Line 522... Line 526...
522
TP-based program using Isabelle's interval

526
TP-based program using Isabelle's interval

523
arithmetic~\cite{hoelzl09realineequalities}, which, after a trial and

527
arithmetic~\cite{hoelzl09realineequalities}, which, after a trial and

524
error optimisation, would lead to a proof that the optimised''

528
error optimisation, would lead to a proof that the optimised''

525
device meets the requirements.

529
device meets the requirements.

526
530
527
\fixme[Provide a detailed example for the inverse problem''.]

-

528
531
\fixme[Provide a detailed example for the inverse problem''.]

-

532