src/HOL/Hoare/README.html
changeset 1335 5e1c0540f285
child 1715 7cbff1da8578
equal deleted inserted replaced
1334:32a9fde85699 1335:5e1c0540f285
       
     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>