6.826—Principles of Computer Systems 1999 Handout 4. Spec Reference Manual 1 4. Spec Reference Manual Spec is a language for writing specifications and the first few stages of successive refinement towards a practical implementation. As a specification language it includes constructs (quanti-fiers, backtracking or non-determinism, some uses of atomic brackets) which are impractical in a final implementation; they are there because they make it easier to write clear, unambiguous and suitably general specifications. If you want to write a practical program, avoid them. This document defines the syntax of the language precisely and the semantics informally. You should read the Introduction to Spec (handout 3) before trying to read this manual. In fact, this manual is intended mainly for reference; rather than reading it carefully, skim through it, and then use the index to find what you need. For a precise definition of the atomic semantics read the forthcoming handout Atomic Semantics of Spec. The handout on Formal Concurrency gives the non-atomic semantics semi-formally. 1. Overview Spec is a notation for writing specifications for a discrete system. What do we mean by a specification? It is the allowed sequences of transitions of a state machine. So Spec is a notation for describing sequences of transitions of a state machine. Expressions and commands The Spec language has two essential parts: An expression describes how to compute a value as a function of other values, either constants or the current values of state variables. A command describes possible transitions, or changes in the values of the state variables. Both are based on the state, which in Spec is a mapping from names to values. The names are called state variables or simply variables: in the examples below they are i and j. There are two kinds of commands: An atomic command describes a set of possible transitions. For instance, the command << i := i + 1 >> describes the transitions i=1→i=2, i=2→i=3, etc. (Actually, many transitions are summarized by i=1→i=2, for instance, (i=1, j=1)→(i=2, j=1) and (i=1, j=15)→(i=2, j=15)). If a command allows more than one transition from a given state we say it is non-deterministic. For instance, the command, << i := 1 [] i := i + 1 >> allows the transitions i=2→i=1 and i=2→i=3. More on this in Atomic Semantics of Spec. A non-atomic command describes a set of sequences of states. More on this in Formal Concurrency. A sequential program, in which we are only interested in the initial and final states, can be described by an atomic command. 6.826—Principles of Computer Systems 1999 Handout 4. Spec Reference Manual 2 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. Organizing a program In addition to the expressions and commands that are the core of the language, Spec has four other mechanisms that are useful for organizing your program and making it easier to understand. A routine is a named computation with parameters (passed by value). There are four kinds: A function is an abstraction of an expression. An atomic procedure is an abstraction of an atomic command. A general procedure is an abstraction of a non-atomic command. A thread is the way to introduce concurrency. A type is a stylized assertion about the set of values that a name can assume. A type is also an easy way to group and name a collection of routines, called its methods, that operate on values in that set. An exception is a way to report an unusual outcome. A module is a way to structure the name space into a two-level hierarchy. An identifier i declared in a module m is known as i in m and as m.i throughout the program. A class is a module that can be instantiated many times to create many objects. A Spec program is some global declarations of variables, routines, types, and exceptions, plus a set of modules each of which declares some variables, routines, types, and exceptions. Outline This manual describes the language bottom-up: Lexical rules Types Expressions Commands Modules At the end there are two sections with additional information: Scope rules Built-in methods for set, sequence, and routine types. There is also an index. The Introduction to Spec has a one-page language summary.6.826—Principles of Computer Systems 1999 Handout 4. Spec Reference Manual 3 2. Grammar rules Nonterminal symbols are in lower case; terminal symbols are punctuation other than ::=, or are quoted, or are in upper case. Alternative choices for a nonterminal are on separate lines. symbol* denotes zero of more occurrences of symbol. The symbol empty denotes the empty string. If x is a nonterminal, the nonterminal xList is defined by xList ::= x x , xList A comment in the grammar runs from % to the end of the line; this is just like Spec itself. A [n] in a comment means that there is an explanation in a note labeled [n] that follows this chunk of grammar. 3. Lexical rules The symbols of the language are literals, identifiers, keywords, operators, and the punctuation ( ) [ ] { } , ; : . | << >> := => -> [] [*]. Symbols must not have embedded white space. They are always taken to be as long as possible. A literal is a decimal number such as 3765, a quoted character such as 'x', or a double-quoted string such as "Hello\n". An identifier (id) is a letter followed by any number of letters, underscores, and digits followed by any number of ' characters. Case is significant in identifiers. By convention type and procedure identifiers begin with a capital letter. An identifier may not be the same as a keyword. The predefined identifiers Any, Bool, Char, Int, Nat, Null, String, true, false, and nil are declared in every program. The meaning of an identifier is established by a declaration; see section 8 on scope for details. Identifiers cannot be redeclared. By convention keywords are written in upper case, but you can write them in lower case if you like; the same strings with mixed case are not keywords, however. The keywords are ALL APROC AS BEGIN BY CLASS CONST DO END ENUM EXCEPT EXCEPTION EXISTS EXPORT FI FUNC HAVOC IF IN IS LAMBDA MODULE OD PROC RAISE RAISES