src/HOL/TLA/README.html
changeset 3807 82a99b090d9d
child 3849 3ea10bfd329d
equal deleted inserted replaced
3806:f371115aed37 3807:82a99b090d9d
       
     1 <HTML><HEAD><TITLE>HOL/TLA/README</TITLE></HEAD><BODY bgcolor="white">
       
     2 
       
     3 <H3>TLA: A formalization of TLA in HOL</H3>
       
     4 
       
     5 Author:     Stephan Merz<BR>
       
     6 Copyright   1997 Universit&auml;t M&uuml;nchen<P>
       
     7 
       
     8 The distribution contains a representation of Lamport's
       
     9 <A HREF="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">
       
    10 Temporal Logic of Actions</A>
       
    11 in Isabelle/HOL.
       
    12 
       
    13 <p>
       
    14 
       
    15 The encoding is mainly oriented towards practical verification
       
    16 examples. It does not contain a formalization of TLA's semantics;
       
    17 instead, it is based on a 
       
    18 <A HREF="doc/PTLA.dvi">complete axiomatization</A> of the "raw"
       
    19 (stuttering-sensitive) variant of propositional TLA. It is
       
    20 accompanied by a
       
    21 <A HREF="doc/design.dvi">design note</A> that explains the basic 
       
    22 setup and use of the prover.
       
    23 
       
    24 <p>
       
    25 
       
    26 The distribution includes the following examples:
       
    27 <UL>
       
    28   <li> a verification of Lamport's <quote>increment</quote> example
       
    29   (subdirectory inc),<P>
       
    30 
       
    31   <li> a proof that two buffers in a row implement a single buffer
       
    32   (subdirectory buffer), and<P>
       
    33 
       
    34    <li> the verification of Broy and Lamport's RPC-Memory example. For details see:<BR>
       
    35 
       
    36         Mart&iacute;n Abadi, Leslie Lamport, and Stephan Merz: 
       
    37         <A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/RPCMemory.html">
       
    38         A TLA Solution to the RPC-Memory Specification Problem</A>.
       
    39         In: <i>Formal System Specification</i>, LNCS 1169, 1996, 21-69.
       
    40 </UL>
       
    41 
       
    42 If you use Isabelle/TLA and have any comments, suggestions or contributions,
       
    43 please contact <A HREF="mailto:merz@informatik.uni-muenchen.de">Stephan Merz</A>.
       
    44 
       
    45 </BODY></HTML>