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