6.826—Principles of Computer Systems 1999 Handout 9. Atomic Semantics of Spec 1 9. Atomic Semantics of Spec This document defines the semantics of the atomic part of the Spec language fairly carefully. It tries to be precise about all difficult points, but is sloppy about some things that seem obvious in order to keep the description short and readable. For the syntax and an informal account of the semantics, see the Spec reference manual, handout 4. There are three reasons for giving a careful semantics of Spec: 1. To give a clear and unambiguous meaning for Spec programs. 2. To make it clear that there is no magic in Spec; its meaning can be given fairly easily and without any exotic methods. 3. To show the versatility of Spec by using it to define itself, which is quite different from the way we use it in the rest of the course. This handout is divided into two parts. In the first half we describe semi-formally the essential ideas and most of the important details. Then in the second half we present the atomic semantics precisely, with a small amount of accompanying explanation. Semi-formal atomic semantics of Spec1 Our purpose is to make it clear that there is no arm waving in the Spec notation that we have given you. A translation of this into fancy words is that we are going to study a formal semantics of the Spec language. Now that is a formidable sounding term, and if you take a course on the semantics of pro-gramming languages (6.821—Gifford, 6.830J—Meyer) you will learn all kinds of fancy stuff about bottom and stack domains and fixed points and things like that. You are not going to see any of that here. We are going to do a very simple minded, garden-variety semantics. We are just going to explain, very carefully and clearly, how it is that every Spec construct can be understood, as a transition of a state machine. So if you understand state machines you should be able to understand all this without any trouble. One reason for doing this is to make sure that we really do know what we are talking about. In general, descriptions of programming languages are not in that state of grace. If you read the Pascal manual or the C manual carefully you will come away with a number of questions about exactly what happens if I do this and this, questions which the manual will not answer adequately. Two reasonably intelligent people who have studied it carefully can come to different conclusions, argue for a long time, and not be able to decide what is the right answer by reading the manual. 1 These semi-formal notes take the form of a dialogue between the lecturer and the class. They were originally written by Mitchell Charity for the 1992 edition of this course, and have been edited for this handout. 6.826—Principles of Computer Systems 1999 Handout 9. Atomic Semantics of Spec 2 There is one class of mechanisms for saying what the computer should do that often does answer your questions precisely, and that is the instruction sets of computers (or, in more modern language, the architecture). These specs are usually written as garden variety state machines with fairly simple transitions, which is not beyond the power of the guy who is writing the manual to describe properly. A programming language, on the other hand, is not like that. It has much more power, generality, and wonderfulness, and also much more room for confusion. Another reason for doing this is to show you that our methods can be applied to a different kind of system than the ones we usually study, that is, to a programming language, a notation for writing programs or a notation for writing specifications. We are going to learn how to write a spec for that particular class of computer systems. This is a very different application of Spec from the one we have just finished looking at, which was file systems. For describing a programming language, Spec is not the ideal descriptive notation. If you were in the business of giving the semantics of programming languages, you wouldn’t use Spec. There are many other notations, some of them better than Spec (although most are far worse). But Spec is good enough; it will do the job. And there is a lot to be said for just having one notation you can use over and over again, as opposed to picking up a new one each time. There are many pitfalls involved in devising a new notation. Those are the two themes of this lecture. We are going to get down to the foundations of Spec, and we are going to see another, very different application of Spec. Certainly a programming language is very different from a file system. For this lecture, we will only talk about the sequential or atomic semantics of Spec, not about concurrent semantics. Consider the program: x, y = 0 thread 1: thread 2: << x := 3 >> << z := x + y >> << y := 4 >> In the concurrent world, it is possible to get any of the answers 0, 3, or 7. In the sequential world, which we are in today, the only possible answers are 0 and 7. It is a simpler world. We will be talking later (in handout 17 on formal concurrency) about the semantics of concurrency, which is unavoidably more complicated. In a sequential Spec program, there are three basic constructs (corresponding to sections 5, 6, and 7 of the reference manual): Expressions Commands Routines In order to describe what each of these things means, we first of all need some notion of what kind of thing the meaning of an expression or command might be. Then we have to explain in detail exactly what the meaning of each possible kind of expression is. The basic technique we use is the standard one for a situation where you have things that are made up out of smaller things: structural induction.6.826—Principles of Computer Systems 1999 Handout 9. Atomic Semantics of Spec 3 The idea of structural induction is this. If you have something which is made up of an A and a B, and you know the meaning of each, and have a way to put them together, you know how to get the meaning of the bigger thing. Some ways to put things together in Spec: A , B A ; B a + b A [] B State What are the meanings going to be? Our basic notion is that what we are doing when writing a Spec program is describing a state machine. The central properties of a state machine are that it has states and it has transitions. State is a function of names to values: State: Name -> Value. For example: VAR x: Int y: Int If there are no other variables,