Subversion Repositories TPPL

Rev

Rev 37 | Show entire file | Ignore whitespace | Details | Blame | Last modification | View Log | RSS feed

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