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