src/HOL/Hoare/README.html
author wenzelm
Mon Mar 22 20:58:52 2010 +0100 (2010-03-22)
changeset 35898 c890a3835d15
parent 15659 043c460af14d
child 38353 d98baa2cf589
permissions -rw-r--r--
recovered header;
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 
     5 <HTML>
     6 
     7 <HEAD>
     8   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     9   <TITLE>HOL/Hoare/ReadMe</TITLE>
    10 </HEAD>
    11 
    12 <BODY>
    13 
    14 <H2>Hoare Logic for a Simple WHILE Language</H2>
    15 
    16 <H3>Language and logic</H3>
    17 
    18 This directory contains an implementation of Hoare logic for a simple WHILE
    19 language. The constructs are
    20 <UL>
    21 <LI> <kbd>SKIP</kbd>
    22 <LI> <kbd>_ := _</kbd>
    23 <LI> <kbd>_ ; _</kbd>
    24 <LI> <kbd>IF _ THEN _ ELSE _ FI</kbd>
    25 <LI> <kbd>WHILE _ INV {_} DO _ OD</kbd>
    26 </UL>
    27 Note that each WHILE-loop must be annotated with an invariant.
    28 <P>
    29 
    30 After loading theory Hoare, you can state goals of the form
    31 <PRE>
    32 VARS x y ... {P} prog {Q}
    33 </PRE>
    34 where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
    35 precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...</kbd> is the
    36 list of all <i>program variables</i> in <kbd>prog</kbd>. The latter list must
    37 be nonempty and it must include all variables that occur on the left-hand
    38 side of an assignment in <kbd>prog</kbd>. Example:
    39 <PRE>
    40 VARS x {x = a} x := x+1 {x = a+1}
    41 </PRE>
    42 The (normal) variable <kbd>a</kbd> is merely used to record the initial
    43 value of <kbd>x</kbd> and is not a program variable. Pre/post conditions
    44 can be arbitrary HOL formulae mentioning both program variables and normal
    45 variables.
    46 <P>
    47 
    48 The implementation hides reasoning in Hoare logic completely and provides a
    49 method <kbd>vcg</kbd> for transforming a goal in Hoare logic into an
    50 equivalent list of verification conditions in HOL:
    51 <PRE>
    52 apply vcg
    53 </PRE>
    54 If you want to simplify the resulting verification conditions at the same
    55 time:
    56 <PRE>
    57 apply vcg_simp
    58 </PRE>
    59 which, given the example goal above, solves it completely. For further
    60 examples see <a href="Examples.html">Examples</a>.
    61 <P>
    62 
    63 IMPORTANT:
    64 This is a logic of partial correctness. You can only prove that your program
    65 does the right thing <i>if</i> it terminates, but not <i>that</i> it
    66 terminates.
    67 
    68 <H3>Notes on the implementation</H3>
    69 
    70 The implementation loosely follows
    71 <P>
    72 Mike Gordon.
    73 <cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
    74 University of Cambridge, Computer Laboratory, TR 145, 1988.
    75 <P>
    76 published as
    77 <P>
    78 Mike Gordon.
    79 <cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
    80 In
    81 <cite>Current Trends in Hardware Verification and Automated Theorem Proving
    82 </cite>,<BR>
    83 edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989. 
    84 <P>
    85 
    86 The main differences: the state is modelled as a tuple as suggested in
    87 <P>
    88 J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
    89 <cite>Mechanizing Some Advanced Refinement Concepts</cite>.
    90 Formal Methods in System Design, 3, 1993, 49-81.
    91 <P>
    92 and the embeding is deep, i.e. there is a concrete datatype of programs. The
    93 latter is not really necessary.
    94 </BODY>
    95 </HTML>