products/sources/formale Sprachen/Isabelle/Doc/Tutorial/document image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: preface.tex   Sprache: Latech

Original von: Isabelle©

\chapter*{Preface}
\markboth{Preface}{Preface}

This volume is a self-contained introduction to interactive proof
in higher-order logic (HOL), using the proof assistant Isabelle. 
It is written for potential users rather
than for our colleagues in the research world.

The book has three parts.  
\begin{itemize}
\item 
The first part, \textbf{Elementary Techniques},
shows how to model functional programs in higher-order logic.  Early
examples involve lists and the natural numbers.  Most proofs
are two steps long, consisting of induction on a chosen variable
followed by the \isa{auto} tactic.  But even this elementary part
covers such advanced topics as nested and mutual recursion.
\item 
The second part, \textbf{Logic and Sets}, presents a collection of
lower-level tactics that you can use to apply rules selectively.  It
also describes Isabelle/HOL's treatment of sets, functions and
relations and explains how to define sets inductively.  One of the
examples concerns the theory of model checking, and another is drawn
from a classic textbook on formal languages.
\item 
The third part, \textbf{Advanced Material}, describes a variety of other
topics.  Among these are the real numbers, records and overloading.  Advanced
techniques for induction and recursion are described.  A whole chapter is
devoted to an extended example: the verification of a security protocol.
\end{itemize}

The typesetting relies on Wenzel's theory presentation tools. An
annotated source file is run, typesetting the theory
in the form of a \LaTeXsource file.  This book is derived almost entirely
from output generated in this way.  The final chapter of Part~I explains how
users may produce their own formal documents in a similar fashion.

Isabelle's \hfootref{https://isabelle.in.tum.de/}{web site} contains
links to the download area and to documentation and other information.
The classic Isabelle user interface is Proof~General~/ Emacs by David
Aspinall's\index{Aspinall, David}. This book says very little about
Proof General, which has its own documentation.

This tutorial owes a lot to the constant discussions with and the valuable
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan
Merz was also kind enough to read and comment on a draft version.  We
received comments from Stefano Bistarelli, Gergely Buday, John Matthews
and Tanja Vos.

The research has been funded by many sources, including the {\sc dfg} grants
NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc
epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and
by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the
\emph{Types} project).

¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff