author nipkow
Thu, 02 May 1996 10:20:15 +0200
changeset 1715 7cbff1da8578
parent 1335 5e1c0540f285
child 5646 7c2ddbaf8b8c
permissions -rw-r--r--
Added note on types.


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

This directory contains a sugared shallow semantic embedding of Hoare logic
for a while language. The implementation closely follows<P>

Mike Gordon.
<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
University of Cambridge, Computer Laboratory, TR 145, 1988.<P>

published as<P>

Mike Gordon.
<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
<cite>Current Trends in Hardware Verification and Automated Theorem Proving
edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989. 

At the top level, it provides a tactic <B>hoare_tac</B>, which transforms a
<KBD>{P} prog {Q}</KBD>
into a set of HOL-level verification conditions.
<DD> the letters a-z are interpreted as program variables,
     all other identifiers as mathematical variables.<P>
The pre/post conditions can be arbitrary HOL formulae including program
variables. The program text should only refer to program variables.
<B>Note</B>: Program variables are typed in the same way as HOL
variables. Although you can write programs over arbitrary types, all
program variables in a particular program must be of the same type!