isabelle: src/HOL/Hoare/README.html@42523fbf643b (annotated)

15283 f21466450330 DOCTYPE declaration added webertj parents: 13875 diff changeset	1	<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added webertj parents: 13875 diff changeset	2
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	3	<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	6	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<TITLE>HOL/Hoare/ReadMe</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	<BODY>
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	11
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	12	<H2>Hoare Logic for a Simple WHILE Language</H2>
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	13
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	14	<H3>Language and logic</H3>
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	15
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	16	This directory contains an implementation of Hoare logic for a simple WHILE
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	17	language. The constructs are
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	18	<UL>
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	19	<LI> <kbd>SKIP</kbd>
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	20	<LI> <kbd>_ := _</kbd>
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	21	<LI> <kbd>_ ; _</kbd>
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	22	<LI> <kbd>IF _ THEN _ ELSE _ FI</kbd>
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	23	<LI> <kbd>WHILE _ INV {_} DO _ OD</kbd>
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	24	</UL>
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	25	Note that each WHILE-loop must be annotated with an invariant.
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	26	<P>
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	27
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	28	After loading theory Hoare, you can state goals of the form
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	29	<PRE>
15659 043c460af14d updated it nipkow parents: 15582 diff changeset	30	VARS x y ... {P} prog {Q}
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	31	</PRE>
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	32	where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	33	precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...</kbd> is the
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	34	list of all <i>program variables</i> in <kbd>prog</kbd>. The latter list must
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	35	be nonempty and it must include all variables that occur on the left-hand
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	36	side of an assignment in <kbd>prog</kbd>. Example:
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	37	<PRE>
15659 043c460af14d updated it nipkow parents: 15582 diff changeset	38	VARS x {x = a} x := x+1 {x = a+1}
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	39	</PRE>
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	40	The (normal) variable <kbd>a</kbd> is merely used to record the initial
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	41	value of <kbd>x</kbd> and is not a program variable. Pre/post conditions
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	42	can be arbitrary HOL formulae mentioning both program variables and normal
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	43	variables.
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	44	<P>
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	45
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	46	The implementation hides reasoning in Hoare logic completely and provides a
15659 043c460af14d updated it nipkow parents: 15582 diff changeset	47	method <kbd>vcg</kbd> for transforming a goal in Hoare logic into an
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	48	equivalent list of verification conditions in HOL:
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	49	<PRE>
15659 043c460af14d updated it nipkow parents: 15582 diff changeset	50	apply vcg
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	51	</PRE>
15659 043c460af14d updated it nipkow parents: 15582 diff changeset	52	If you want to simplify the resulting verification conditions at the same
043c460af14d updated it nipkow parents: 15582 diff changeset	53	time:
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	54	<PRE>
15659 043c460af14d updated it nipkow parents: 15582 diff changeset	55	apply vcg_simp
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	56	</PRE>
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	57	which, given the example goal above, solves it completely. For further
15659 043c460af14d updated it nipkow parents: 15582 diff changeset	58	examples see <a href="Examples.html">Examples</a>.
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	59	<P>
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	60
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	61	IMPORTANT:
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	62	This is a logic of partial correctness. You can only prove that your program
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	63	does the right thing <i>if</i> it terminates, but not <i>that</i> it
7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	64	terminates.
72806 4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	65	A logic of total correctness is also provided and described below.
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	66
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	67	<H3>Total correctness</H3>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	68
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	69	To prove termination, each WHILE-loop must be annotated with a variant:
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	70	<UL>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	71	<LI> <kbd>WHILE _ INV {_} VAR {_} DO _ OD</kbd>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	72	</UL>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	73	A variant is an expression with type <kbd>nat</kbd>, which may use program
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	74	variables and normal variables.
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	75	<P>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	76
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	77	A total-correctness goal has the form
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	78	<PRE>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	79	VARS x y ... [P] prog [Q]
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	80	</PRE>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	81	enclosing the pre- and postcondition in square brackets.
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	82	<P>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	83
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	84	Methods <kbd>vcg_tc</kbd> and <kbd>vcg_tc_simp</kbd> can be used to derive
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	85	verification conditions.
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	86	<P>
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	87
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	88	From a total-correctness proof, a function can be extracted which
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	89	for every input satisfying the precondition returns an output
4fa08e083865 Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann nipkow parents: 38353 diff changeset	90	satisfying the postcondition.
5646 7c2ddbaf8b8c New many-sorted version. nipkow parents: 1715 diff changeset	91
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	92	<H3>Notes on the implementation</H3>
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	93
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	94	The implementation loosely follows
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	95	<P>
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	96	Mike Gordon.
5e1c0540f285 New directory. nipkow parents: diff changeset	97	<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	98	University of Cambridge, Computer Laboratory, TR 145, 1988.
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	99	<P>
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	100	published as
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	101	<P>
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	102	Mike Gordon.
5e1c0540f285 New directory. nipkow parents: diff changeset	103	<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
5e1c0540f285 New directory. nipkow parents: diff changeset	104	In
5e1c0540f285 New directory. nipkow parents: diff changeset	105	<cite>Current Trends in Hardware Verification and Automated Theorem Proving
5e1c0540f285 New directory. nipkow parents: diff changeset	106	</cite>,<BR>
5e1c0540f285 New directory. nipkow parents: diff changeset	107	edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.
5e1c0540f285 New directory. nipkow parents: diff changeset	108	<P>
5e1c0540f285 New directory. nipkow parents: diff changeset	109
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	110	The main differences: the state is modelled as a tuple as suggested in
1715 7cbff1da8578 Added note on types. nipkow parents: 1335 diff changeset	111	<P>
5647 4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	112	J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	113	<cite>Mechanizing Some Advanced Refinement Concepts</cite>.
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	114	Formal Methods in System Design, 3, 1993, 49-81.
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	115	<P>
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	116	and the embeding is deep, i.e. there is a concrete datatype of programs. The
4e8837255b87 Description of new version. nipkow parents: 5646 diff changeset	117	latter is not really necessary.
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	118	</BODY>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	119	</HTML>

author	haftmann
	Mon, 13 Sep 2021 14:18:24 +0000
changeset 74309	42523fbf643b
parent 72806	4fa08e083865
permissions	-rw-r--r--