src/HOL/Hoare/README.html
changeset 5646 7c2ddbaf8b8c
parent 1715 7cbff1da8578
child 5647 4e8837255b87
equal deleted inserted replaced
5645:b872b209db69 5646:7c2ddbaf8b8c
     1 <HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
     1 <HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
     2 
     2 
     3 <H2>Semantic Embedding of Hoare Logic</H2>
     3 <H2>Hoare Logic for a Simple WHILE Language</H2>
       
     4 
       
     5 <H1>The language and logic<H1>
       
     6 
       
     7 This directory contains an implementation of Hoare logic for a simple WHILE
       
     8 language. The  are
       
     9 <UL>
       
    10 <LI> SKIP
       
    11 <LI> _ := _
       
    12 <LI> _ ; _
       
    13 <LI> <kbd>IF _ THEN _ ELSE _ FI<kbd>
       
    14 <LI> WHILE _ INV {_} DO _ OD
       
    15 </UL>
       
    16 Note that each WHILE-loop must be annotated with an invariant.
       
    17 <P>
       
    18 
       
    19 After loading theory Hoare, you can state goals of the form
       
    20 <PRE>
       
    21 |- VARS x y ... . {P} prog {Q}
       
    22 </PRE>
       
    23 where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
       
    24 precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...<kbd> is the
       
    25 list of all <i>program variables</i> in <kbd>prog</kbd>. The latter list must
       
    26 be nonempty and it must include all variables that occur on the left-hand
       
    27 side of an assignment in <kbd>prof</kbd>. Example:
       
    28 <PRE>
       
    29 |- VARS x. {x = a} x := x+1 {x = a+1}
       
    30 </PRE>
       
    31 The (normal) variable <kbd>a</kbd> is merely used to record the initial
       
    32 value of <kbd>x</kbd> and is not a program variable. Pre and postconditions
       
    33 can be arbitrary HOL formulae mentioning both program variables and normal
       
    34 variables.
       
    35 <P>
       
    36 
       
    37 The implementation hides reasoning in Hoare logic completely and provides a
       
    38 tactic hoare_tac for generating the verification conditions in ordinary
       
    39 logic:
       
    40 <PRE>
       
    41 by(hoare_tac tac i);
       
    42 </PRE>
       
    43 applies the tactic to subgoal <kbd>i</kbd> and applies the parameter
       
    44 <kbd>tac</kbd> to all generated verification conditions. A typical call is
       
    45 <PRE>
       
    46 by(hoare_tac Asm_full_simp_tac 1);
       
    47 </PRE>
       
    48 which, given the example goal above, solves it completely.
       
    49 <P>
       
    50 
       
    51 IMPORTANT:
       
    52 This is a logic of partial correctness. You can only prove that your program
       
    53 does the right thing <i>if</i> it terminates, but not <i>that</i> it
       
    54 terminates.
       
    55 
       
    56 <H1>Notes on the implementation</H1>
     4 
    57 
     5 This directory contains a sugared shallow semantic embedding of Hoare logic
    58 This directory contains a sugared shallow semantic embedding of Hoare logic
     6 for a while language. The implementation closely follows<P>
    59 for a while language. The implementation closely follows<P>
     7 
    60 
     8 
    61