summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Hoare/README.html

author | berghofe |

Tue, 25 Jun 1996 13:11:29 +0200 | |

changeset 1824 | 44254696843a |

parent 1715 | 7cbff1da8578 |

child 5646 | 7c2ddbaf8b8c |

permissions | -rw-r--r-- |

Changed argument order of nat_rec.

<HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY> <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> In <cite>Current Trends in Hardware Verification and Automated Theorem Proving </cite>,<BR> edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989. <P> At the top level, it provides a tactic <B>hoare_tac</B>, which transforms a goal <BLOCKQUOTE> <KBD>{P} prog {Q}</KBD> </BLOCKQUOTE> into a set of HOL-level verification conditions. <DL> <DT>Syntax: <DD> the letters a-z are interpreted as program variables, all other identifiers as mathematical variables.<P> </DL> The pre/post conditions can be arbitrary HOL formulae including program variables. The program text should only refer to program variables. <P> <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! </BODY></HTML>