-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathbook9020.html
225 lines (176 loc) · 5.96 KB
/
book9020.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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
<!DOCTYPE html>
<HTML>
<!-- Mirrored from lamport.azurewebsites.net/tla/book.html?back-link=learning.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:34:27 GMT -->
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<META NAME="GENERATOR" CONTENT="Mozilla/4.05 [en] (X11; I; OSF1 V4.0 alpha)
[Netscape]">
<!--
%&b&<b>#</b>&
%&c& <b>#</b> &
-->
<!-- The following loads the style sheet for the html files of
the tla web site -->
<link rel="stylesheet" type="text/css" href="tlaweb.css">
<!-- FILE SPECIFIC STYLE DECLARATIONS -->
<style>
H4 { margin-top:13px;
margin-bottom:5px}
DD {margin-bottom:-5px}
</style>
<script src="tlaweb.js"> </script>
<title>Specifying Systems</title>
</HEAD>
<BODY BGCOLOR=#fffff0 onload="initialize()">
<table id="main">
<tr>
<td id="main_leftcolumn" >
</td>
<td id="main_contentcolumn">
<table>
<tr >
<td style="vertical-alight:top">
<div id = "showleftcol"> </div>
<H1>Specifying Systems</H1>
<p style="margin-top:-8px; margin-bottom:-18px">
Leslie Lamport<p>
<font size=-1><I> Last modified on 26 January 2020</I></font>
</td>
<td style="vertical-alight:top;width:auto">
</td>
</tr>
</table>
<HR style="margin-bottom:12px;margin-top:-11px">
<TABLE>
<TR VALIGN=TOP>
<TD>
<IMG SRC= "book-cover.jpg" alt = "" width = "125">
</TD>
<TD>
<PRE> </PRE>
</TD>
<TD WIDTH = "500">
<FONT size=+1> This book won an award for its cover design
at the New England Book Show. A production editor at Addison-Wesley wrote:
<BLOCKQUOTE style="margin-top:8px">
For those of you who are unfamiliar with the Book Show, I think of it
as the Emmys of book production. Many different publishers
participate, competition is steep, and there [are] often hundreds of
nominations for the judges to review.
</BLOCKQUOTE>
</FONT>
</TD>
</TR>
</TABLE>
<HR style="margin-bottom:-5px;margin-top:-5px">
<BR>
The book <I>Specifying Systems: The TLA+ Language and Tools for
Hardware and Software Engineers</I> has been published by
Addison-Wesley Professional, a division of Pearson Education.
You can <A HREF="http://www.informit.com/store/specifying-systems-the-tla-plus-language-and-tools-9780321143068">click
here</A> to order it from the publisher, or
<A HREF = "#download">download</A> a copy for your own use. You
can also download
<a href="#accompanying">accompanying material</a>.
<!-- Please address all comments and suggestions to
<A HREF ="http://lamport.org">Leslie Lamport</A>.
-->
<H4>The Book</H4>
The book is 364 pages long (including a 17-page index).
However, most people will want to read only the first part, which
comprises the first seven chapters and is 83 pages long.
Here is the list of chapters.
<OL style="margin-top:10px">
<LI> A Little Simple Math
<LI> Specifying a Simple Clock
<LI> An Asynchronous Interface
<LI> A FIFO
<LI> A Caching Memory
<LI> Some More Math
<LI> Writing a Specification: Some Advice
<LI> Liveness and Fairness
<LI> Real Time
<LI> Composing Specifications
<LI> Advanced Examples
<LI> The Syntactic Analyzer
<LI> The TLATeX Typesetter
<LI> The TLC Model Checker
<LI> The Syntax of TLA+
<LI> The Operators of TLA+
<LI> The Meaning of a Module
<LI> The Standard Modules
</OL>
<p>
<H4>The List of Corrections</H4>
This is a list of all known errors and omissions in the
book. If you are the first to report an error, you will be
acknowledged in any new edition.
<H4><a name="accompanying">Accompanying Material</a></H4>
Also available for downloading is material to accompany the book.
This includes the ASCII versions of all specifications from the book,
additional modules and configuration files for using the TLC model
checker to check some of the specifications, and a few
exercises.
<!--
I hope that readers will provide additional exercises.
I would also like to include example specifications written by
others.
Now, the only other example is the
<A HREF = "wildfire-challenge.html">Wildfire
challenge problem</A>.
The specification of the Alpha memory that it contains will be of
particular interest to readers of the memory specifications in Chapter
11.
Please contact me if you have any suggestions.
-->
<p>
The material is organized hierarchically, with the material for each
chapter in a separate folder (directory).
Each folder, including the root, has a README file containing the
exercises and an explanation of what else is in the
directory.
The material is available as a Zip file for Windows users and as a
gzipped tar file for Unix users.
<H3><A NAME = "download">Downloading</A></H3>
<DL>
<DT> The Book
<DD>
The book <I>Specifying Systems: The TLA+ Language and Tools for
Hardware and Software Engineers</I> by Leslie Lamport is copyright (c)
2002 by Pearson Education, Inc. It may not be reproduced
or distributed for commercial purposes, or for any purpose other than
for personal use, without the prior written permission of the
publisher. <BR>
<A HREF = "book-02-08-08.ps">Postscript</A>
<A HREF = "book-02-08-08.ps.gz">Gzipped Postscript</A>
<A HREF = "book-02-08-08.pdf">PDF</A>
<P>
<DT>The List of Corrections
<DD> <A HREF = "errata.pdf">PDF</A>
<P>
<DT>The Supporting Material
<DD> <DD>
<A HREF="web.zip">Windows Zip File</A>
<A HREF="web.tar.gz">Unix Gzipped Tar File</A>
<p>
<DT>An
<A href="https://github.com/jackfoxy/SpecifyingSystemsWithContents">
alternative pdf version</A>
with the table of contents as bookmarks.
</DL>
</TD>
</TR>
<!-- Bottom Back button -->
<tr>
<td>
<a class="back-link" style="display:none" href="#">
<p style="margin-top:-50px"><b>Back</b>
</p>
</a>
</td>
</tr>
</TABLE>
</BODY>
<!-- Mirrored from lamport.azurewebsites.net/tla/book.html?back-link=learning.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:37:31 GMT -->
</HTML>