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