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