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