|
1335
|
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, Springer-Verlag, 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 HOL-level verification conditions.
|
|
|
29 |
<DL>
|
|
|
30 |
<DT>Syntax:
|
|
|
31 |
<DD> the letters a-z 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>
|