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 WHILEloop 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 lefthand 

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 