6.826—Principles of Computer Systems 2004 Handout 3. Introduction to Spec 1 3. Introduction to Spec This handout explains what the Spec language is for, how to use it effectively, and how it differs from a programming language like C, Pascal, Clu, Java, or Scheme. Spec is very different from these languages, but it is also much simpler. Its meaning is clearer and Spec programs are more succinct and less burdened with trivial details. The handout also introduces the main constructs that are likely to be unfamiliar to a programmer. You will probably find it worthwhile to read it over more than once, until those constructs are familiar. Don’t miss the one-page summary of spec at the end. The handout also has an index. Spec is a language for writing precise descriptions of digital systems, both sequential and concurrent. In Spec you can write something that differs from practical code (for instance, code written in C) only in minor details of syntax. This sort of thing is usually called a program. Or you can write a very high level description of the behavior of a system, usually called a specification. A good specification is almost always quite different from a good program. You can use Spec to write either one, but not the same style of Spec. The flexibility of the language means that you need to know the purpose of your Spec in order to write it well. Most people know a lot more about writing programs than about writing specs, so this introduction emphasizes how Spec differs from a programming language and how to use it to write good specs. It does not attempt to be either complete or precise, but other handouts fill these needs. The Spec Reference Manual (handout 4) describes the language completely; it gives the syntax of Spec precisely and the semantics informally. Atomic Semantics of Spec (handout 9) describes precisely the meaning of an atomic command; here ‘precisely’ means that you should be able to get an unambiguous answer to any question. The section “Non-Atomic Semantics of Spec” in handout 17 on formal concurrency describes the meaning of a non-atomic command. Spec’s notation for commands, that is, for changing the state, is derived from Edsger Dijkstra’s guarded commands (E. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976) as extended by Greg Nelson (G. Nelson, A generalization of Dijkstra’s calculus, ACM TOPLAS 11, 4, Oct. 1989, pp 517-561). The notation for expressions is derived from mathematics. This handout starts with a discussion of specifications and how to write them, with many small examples of Spec. Then there is an outline of the Spec language, followed by three extended examples of specs and code. At the end are two handy tear-out one-page summaries, one of the language and one of the official POCS strategy for writing specs and code. 6.826—Principles of Computer Systems 2004 Handout 3. Introduction to Spec 2 What is a specification for? The purpose of a specification is to communicate precisely all the essential facts about the behavior of a system. The important words in this sentence are: communicate The spec should tell both the client and the implementer what each needs to know. precisely We should be able to prove theorems or compile machine instructions based on the spec. essential Unnecessary requirements in the spec may confuse the client or make it more expensive to implement the system. behavior We need to know exactly what we mean by the behavior of the system. Communication Spec mediates communication between the client of the system and its implementer. One way to view the spec is as a contract between these parties: The client agrees to depend only on the system behavior expressed in the spec; in return it only has to read the spec, and it can count on the implementer to provide a system that actually does behave as the spec says it should. The implementer agrees to provide a system that behaves according to the spec; in return it is free to arrange the internals of the system however it likes, and it does not have to deliver anything not laid down in the spec. Usually the implementer of a spec is a programmer, and the client is another programmer. Usually the implementer of a program is a compiler or a computer, and the client is a programmer. Usually the system that the implementer provides is called an implementation, but in this course we will call it code for short. It doesn’t have to be C or Java code; we will give lots of examples of code in Spec which would still require a lot of work on the details of data structures, memory allocation, etc. to turn it into an executable program. You might wonder what good this kind of high-level code is. It expresses the difficult parts of the design clearly, without the straightforward details needed to actually make it run. Behavior What do we mean by behavior? In real life a spec defines not only the functional behavior of the system, but also its performance, cost, reliability, availability, size, weight, etc. In this course we will deal with these matters informally if at all. The Spec language doesn’t help much with them. Spec is concerned only with the possible state transitions of the system, on the theory that the possible state transitions tell the complete story of the functional behavior of a digital system. So we make the following definitions:6.826—Principles of Computer Systems 2004 Handout 3. Introduction to Spec 3 A state is the values of a set of names (for instance, x=3, color=red). A history is a sequence of states such that each pair of adjacent states is a transition of the system (for instance, x=1; x=2; x=5 is the history if the initial state is x=1 and the transitions are “if x = 1 then x := x + 1” and “if x = 2 then x := 2 * x + 1”). A behavior is a set of histories (a non-deterministic system can have more than one history, usually at least one for every possible input). How can we specify a behavior? One way to do this is to just write down all the histories in the behavior. For example, if the state just consists of a single integer, we might write 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 ... 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 .... 1 2 3 4 5 1 2 3 1 2 3 4 5 6 7 8 9 10 The example reveals two problems with this approach: The sequences are long, and there are a lot of them, so it takes a