src/HOL/TLA/README.html
author merz
Mon Oct 13 11:00:06 1997 +0200 (1997-10-13)
changeset 3849 3ea10bfd329d
parent 3807 82a99b090d9d
child 5383 74c2da44d144
permissions -rw-r--r--
Absolute URL's for documentation
     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 although it could be an interesting exercise to add such a formalization
    18 to the existing representation. Instead, it is based on a 
    19 <A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/ptla.ps">complete axiomatization</A>
    20 of the "raw" (stuttering-sensitive) variant of propositional TLA. 
    21 There is also a
    22 <A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/IsaTLADesign.ps">design note</A> 
    23 that explains the basic setup and use of the prover.
    24 
    25 <p>
    26 
    27 The distribution includes the following examples:
    28 <UL>
    29   <li> a verification of Lamport's <quote>increment</quote> example
    30   (subdirectory inc),<P>
    31 
    32   <li> a proof that two buffers in a row implement a single buffer
    33   (subdirectory buffer), and<P>
    34 
    35    <li> the verification of Broy and Lamport's RPC-Memory example. For details see:<BR>
    36 
    37         Mart&iacute;n Abadi, Leslie Lamport, and Stephan Merz: 
    38         <A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/RPCMemory.html">
    39         A TLA Solution to the RPC-Memory Specification Problem</A>.
    40         In: <i>Formal System Specification</i>, LNCS 1169, 1996, 21-69.
    41 </UL>
    42 
    43 If you use Isabelle/TLA and have any comments, suggestions or contributions,
    44 please contact <A HREF="mailto:merz@informatik.uni-muenchen.de">Stephan Merz</A>.
    45 
    46 </BODY></HTML>