src/HOL/Hoare/README.html
author wenzelm
Fri, 29 May 1998 13:50:21 +0200
changeset 4987 257aeccdefc3
parent 1715 7cbff1da8578
child 5646 7c2ddbaf8b8c
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     1
<HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     3
<H2>Semantic Embedding of Hoare Logic</H2>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     4
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     5
This directory contains a sugared shallow semantic embedding of Hoare logic
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     6
for a while language. The implementation closely follows<P>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     7
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     9
Mike Gordon.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    11
University of Cambridge, Computer Laboratory, TR 145, 1988.<P>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    12
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    13
published as<P>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    14
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    15
Mike Gordon.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    16
<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    17
In
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    18
<cite>Current Trends in Hardware Verification and Automated Theorem Proving
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    19
</cite>,<BR>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    20
edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989. 
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    21
<P>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    22
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    23
At the top level, it provides a tactic <B>hoare_tac</B>, which transforms a
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    24
goal
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    25
<BLOCKQUOTE>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    26
<KBD>{P} prog {Q}</KBD>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    27
</BLOCKQUOTE>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    28
into a set of HOL-level verification conditions.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    29
<DL>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    30
<DT>Syntax:
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    31
<DD> the letters a-z are interpreted as program variables,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    32
     all other identifiers as mathematical variables.<P>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    33
</DL>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    34
The pre/post conditions can be arbitrary HOL formulae including program
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    35
variables. The program text should only refer to program variables.
1715
7cbff1da8578 Added note on types.
nipkow
parents: 1335
diff changeset
    36
<P>
7cbff1da8578 Added note on types.
nipkow
parents: 1335
diff changeset
    37
<B>Note</B>: Program variables are typed in the same way as HOL
7cbff1da8578 Added note on types.
nipkow
parents: 1335
diff changeset
    38
variables. Although you can write programs over arbitrary types, all
7cbff1da8578 Added note on types.
nipkow
parents: 1335
diff changeset
    39
program variables in a particular program must be of the same type!
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    40
</BODY></HTML>