summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 29 Jan 2001 18:56:37 +0100 | |

changeset 10993 | 883248dcf3f8 |

parent 10992 | 0932a82022fd |

child 10994 | 9429f2e7d16a |

added Unix example;

--- a/doc-src/IsarRef/intro.tex Mon Jan 29 14:14:17 2001 +0100 +++ b/doc-src/IsarRef/intro.tex Mon Jan 29 18:56:37 2001 +0100 @@ -255,15 +255,27 @@ big mathematics application on infinitary vector spaces and functional analysis. \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental - properties of $\lambda$-calculus (Church-Rosser and termination). This may - serve as a realistic example of porting of legacy proof scripts into Isar - tactic emulation scripts. + properties of $\lambda$-calculus (Church-Rosser and termination). + + This may serve as a realistic example of porting of legacy proof scripts + into Isar tactic emulation scripts. +\item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical + model of the main aspects of the Unix file-system including its security + model, but ignoring processes. A few odd effects caused by the general + ``worse-is-better'' approach followed in Unix are discussed within the + formal model. + + This example represents a non-trivial verification task, with all proofs + carefully worked out using the proper part of the Isar proof language; + unstructured scripts are only used for symbolic evaluation. \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight - bytecode verifier, including proofs of type-safety. This represents a very - ``realistic'' example of large formalizations performed in either form of - legacy scripts, tactic emulation scripts, and proper Isar proof texts. + bytecode verifier, including proofs of type-safety. + + This represents a very ``realistic'' example of large formalizations + performed in either form of legacy scripts, tactic emulation scripts, and + proper Isar proof texts. \end{itemize}