-
Notifications
You must be signed in to change notification settings - Fork 1
/
notes.html
102 lines (82 loc) · 3.91 KB
/
notes.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
<title>TLA Notes</title>
<H1>TLA NOTES</H1>
<I>Last modified 5 January 2019</I>
<HR>
This is a collection of material about
<A HREF = "tla.html">TLA (Temporal Logic of Actions)</A>
and specification in general that may be of interest, but has not
appeared in a real paper. These notes are rough and half-baked; they
probably contain many errors. But, they provide the only available
information on several important topics. <P>
The notes marked "LaTeX/ASCII" can be read in ASCII or run through
LaTeX to get a somewhat more readable version. To run them
through LaTeX, you need the style file
<A HREF = "http://lamport.azurewebsites.net/latex/spec92.sty"> <B>spec92.sty</B></A>.
You can <A HREF = "notes/reading.txt">click here</A> for an explanation
of the ASCII conventions that are used.
<HR>
<DL>
<DT> <B>A Completeness Theorem for TLA</B> <BR>
<I>17 November 1993, LaTeX formatting corrected 5 January 2019</I>
<DD> A relative completeness theorem for TLA, with its proof.
The first part was distributed to the TLA mailing list.
For intrepid souls only.<BR>
<A HREF = "notes/complete.tex">LaTeX/ASCII</A>
<A HREF = "notes/complete.pdf">pdf version</A>
<P>
<DT> <B>Types Considered Harmful</B> <BR>
Leslie Lamport <BR>
<I>23 December 1992</I>
<DD> A brief explanation of how to do mathematics without types.
(10 pages) <BR>
<A HREF = "notes/types.ps.z">Postscript</A> -
<A HREF = "notes/types.dvi.z">DVI</A> -
<A HREF = "notes/types.tex.z">LaTeX</A><P>
<DT><B>Using Tense Logic in Specification and Verification </B> <BR>
Peter Ladkin<BR>
<I>5 August 1993</I>
<DD> These are Peter Ladkin's comments on the question of using
first-order logic rather than TLA. (Sent to TLA mailing list.) <BR>
<A HREF = "notes/93-08-05.tex">LaTeX/ASCII</A><P>
<DT><B>Miscellany </B> <BR>
<I>21 June 1993</I>
<DD>Contains "Some Thoughts on Specification"
(a short, not-too-hot flame),
"Thinking About Actions Instead of States" (of interest to people who
want to write TLA specs), "Encoding TLA in Ordinary Math" (required
reading for anyone involved in mechanizing TLA), and "A New TLA+
Construct" (for aficionados of TLA+). (Sent to TLA mailing list.)<BR>
<A HREF = "notes/93-06-21.tex">LaTeX/ASCII</A><P>
<DT><B> Some Thoughts on Specification</B> <BR>
<I>5 May 1992</I>
<DD> Some philosophical musings about specification.
(Sent to TLA mailing list.) <BR>
<A HREF = "notes/92-05-05.txt">ASCII</A><P>
<DT><B> The Reduction Theorem </B> <BR>
<I>12 April 1992</I>
<DD> The Reduction Theorem allows one to prove things about
a fine-grained specification by reasoning about a
coarser-grained one. This may be a crucial result
for carrying verification down to the level of executable
code. (Sent to TLA mailing list.) <BR>
<A HREF = "notes/reduction.tex">LaTeX/ASCII</A><P>
<DT><B> The Existence of Refinement Mappings </B> <BR>
<I>19 March 1992</I>
<DD> An attempt to redo the paper of the same name in
TLA. It contains mistakes, and there should soon be
a paper that does this. (Sent to TLA mailing list.) <BR>
<A HREF = "notes/92-03-19.tex">LaTeX/ASCII</A><P>
<DT><B> Miscellany </B> <BR>
<I>4 April 1991</I>
<DD> Contains a discussion of why breaking closed systems into open
components makes for more work, and a
representation of the closure and realizable-part operators in TLA.
(Sent to TLA mailing list.) <BR>
<A HREF = "notes/91-04-21.txt">ASCII</A><P>
<DT><B> Philosophical Hogwash</B> <BR>
<I>15 November 1990</I>
<DD> Some musings sent to the concurrency mailing list in
response to a message from Vaughan Pratt.
(Sent to TLA mailing list.) <BR>
<A HREF = "notes/90-11-15a.txt">ASCII</A><P>
</DL>