NameDateSize

..30-Oct-2020171

Arith2.thyH A D25-Jul-20192.2 KiB

document/H25-Jul-20194

Examples.thyH A D25-Jul-20198.8 KiB

ExamplesAbort.thyH A D25-Jul-2019567

Heap.thyH A D25-Jul-20195.8 KiB

HeapSyntax.thyH A D25-Jul-20191,012

HeapSyntaxAbort.thyH A D25-Jul-20191.5 KiB

Hoare.thyH A D25-Jul-2019191

Hoare_Logic.thyH A D25-Jul-20193.9 KiB

Hoare_Logic_Abort.thyH A D25-Jul-20195 KiB

hoare_syntax.MLH A D25-Jul-20195.4 KiB

hoare_tac.MLH A D25-Jul-20197.6 KiB

Pointer_Examples.thyH A D25-Jul-201917.9 KiB

Pointer_ExamplesAbort.thyH A D25-Jul-2019827

Pointers0.thyH A D25-Jul-201913.2 KiB

README.htmlH A D25-Jul-20192.8 KiB

SchorrWaite.thyH A D25-Jul-201927.6 KiB

Separation.thyH A D25-Jul-20196.8 KiB

SepLogHeap.thyH A D25-Jul-20193.1 KiB

README.html

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
16This directory contains an implementation of Hoare logic for a simple WHILE
17language. 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>
25Note that each WHILE-loop must be annotated with an invariant.
26<P>
27
28After loading theory Hoare, you can state goals of the form
29<PRE>
30VARS x y ... {P} prog {Q}
31</PRE>
32where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
33precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...</kbd> is the
34list of all <i>program variables</i> in <kbd>prog</kbd>. The latter list must
35be nonempty and it must include all variables that occur on the left-hand
36side of an assignment in <kbd>prog</kbd>. Example:
37<PRE>
38VARS x {x = a} x := x+1 {x = a+1}
39</PRE>
40The (normal) variable <kbd>a</kbd> is merely used to record the initial
41value of <kbd>x</kbd> and is not a program variable. Pre/post conditions
42can be arbitrary HOL formulae mentioning both program variables and normal
43variables.
44<P>
45
46The implementation hides reasoning in Hoare logic completely and provides a
47method <kbd>vcg</kbd> for transforming a goal in Hoare logic into an
48equivalent list of verification conditions in HOL:
49<PRE>
50apply vcg
51</PRE>
52If you want to simplify the resulting verification conditions at the same
53time:
54<PRE>
55apply vcg_simp
56</PRE>
57which, given the example goal above, solves it completely. For further
58examples see <a href="Examples.html">Examples</a>.
59<P>
60
61IMPORTANT:
62This is a logic of partial correctness. You can only prove that your program
63does the right thing <i>if</i> it terminates, but not <i>that</i> it
64terminates.
65
66<H3>Notes on the implementation</H3>
67
68The implementation loosely follows
69<P>
70Mike Gordon.
71<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
72University of Cambridge, Computer Laboratory, TR 145, 1988.
73<P>
74published as
75<P>
76Mike Gordon.
77<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
78In
79<cite>Current Trends in Hardware Verification and Automated Theorem Proving
80</cite>,<BR>
81edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989. 
82<P>
83
84The main differences: the state is modelled as a tuple as suggested in
85<P>
86J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
87<cite>Mechanizing Some Advanced Refinement Concepts</cite>.
88Formal Methods in System Design, 3, 1993, 49-81.
89<P>
90and the embeding is deep, i.e. there is a concrete datatype of programs. The
91latter is not really necessary.
92</BODY>
93</HTML>
94