Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

版本说明：1

作     者：Leslie Lamport 

I S B N：(纸本) 9780321143068 

出 版 社：Addison-Wesley 

出 版 年：2002年

主 题 词：Logic Logic Foundations of Mathematics Computer Architecture/Engineering 

摘      要：From the Book: This book will teach you how to write specifications of computer systems, using the language TLA+. It s rather long, but most people will read only Part I, which comprises the first 83 pages. That part contains all that most engineers need to know about writing specifications; it assumes only the basic background in computing and knowledge of mathematics expected of an undergraduate studying engineering or computer science. Part II contains more advanced material for more sophisticated readers. The remainder of the book is a reference manualPart III for the TLA+ tools and Part IV for the language itself. The TLA World Wide Web page contains material to accompany the book, including the TLA+ tools, exercises, references to the literature, and a list of corrections. There is a link to the TLA Web page on http://***. What Is a Specification Writing is nature s way of letting you know how sloppy your thinking is.-Guindon A specification is a written description of what a system is supposed to do. Specifying a system helps us understand it. It s a good idea to understand a system before building it, so it s a good idea to write a specification of a system before implementing it. This book is about specifying the behavioral properties of a systemalso called its functional or logical properties. These are the properties that specify what the system is supposed to do. There are other important kinds of properties that we don t consider, including performance properties. Worst-case performance can often be expressed as a behavioral propertyforexample, Chapter 9 explains how to specify that a system must react within a certain length of time. However, specifying average performance is beyond the scope of the methods described here. Our basic tool for writing specifications is mathematics. Mathematics is nature s way of letting you know how sloppy your writing is. It s hard to be precise in an imprecise language like English or Chinese. In engineering, i