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