equal
deleted
inserted
replaced

1 <HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY> 

2 

3 <H2>Semantic Embedding of Hoare Logic</H2> 

4 

5 This directory contains a sugared shallow semantic embedding of Hoare logic 

6 for a while language. The implementation closely follows<P> 

7 

8 

9 Mike Gordon. 

10 <cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR> 

11 University of Cambridge, Computer Laboratory, TR 145, 1988.<P> 

12 

13 published as<P> 

14 

15 Mike Gordon. 

16 <cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR> 

17 In 

18 <cite>Current Trends in Hardware Verification and Automated Theorem Proving 

19 </cite>,<BR> 

20 edited by G. Birtwistle and P.A. Subrahmanyam, SpringerVerlag, 1989. 

21 <P> 

22 

23 At the top level, it provides a tactic <B>hoare_tac</B>, which transforms a 

24 goal 

25 <BLOCKQUOTE> 

26 <KBD>{P} prog {Q}</KBD> 

27 </BLOCKQUOTE> 

28 into a set of HOLlevel verification conditions. 

29 <DL> 

30 <DT>Syntax: 

31 <DD> the letters az are interpreted as program variables, 

32 all other identifiers as mathematical variables.<P> 

33 </DL> 

34 The pre/post conditions can be arbitrary HOL formulae including program 

35 variables. The program text should only refer to program variables. 

36 </BODY></HTML> 