Operational Rules

Equipped with environments, stores, objects, and class definitions, we can now attack the operational semantics for Cool. The operational semantics is described by rules similar to the rules used in type checking. The general form of the rules is:

$$\frac{\vdots}{so,S,E\vdash e_1 : v,S'}\eqno \mbox{}$$

The rule should be read as: In the context where self is the object $so$, the store is $S$, and the environment is $E$, the expression $e_1$ evaluates to object $v$ and the new store is $S'$. The dots above the horizontal bar stand for other statements about the evaluation of sub-expressions of $e_1$.

Besides an environment and a store, the evaluation context contains a self object $so$. The self object is just the object to which the identifier self refers if self appears in the expression. We do not place self in the environment and store because self is not a variable--it cannot be assigned to. Note that the rules specify a new store after the evaluation of an expression. The new store contains all changes to memory resulting as side effects of evaluating expression $e_1$.

The rest of this section presents and briefly discusses each of the operational rules. A few cases are not covered; these are discussed at the end of the section.

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : v_1,S_2\\ E(I... ...o,S_1,E\vdash Id\leftarrow e_1 : v_1,S_3}\eqno \mbox{[Assign]}$$

An assignment first evaluates the expression on the right-hand side, yielding a value $v_1$. This value is stored in memory at the address for the identifier.

The rules for identifier references, self, and constants are straightforward:

$$\frac{\begin{array}{l} E(Id) = l\\ S(l) = v \end{array}}{so,S,E\vdash Id : v,S}\eqno \mbox{[Var]}$$

$$\frac{}{so,S,E\vdash \mbox{self} : so,S}\eqno \mbox{[Self]}$$

$$\frac{}{so,S,E\vdash \mbox{true} : Bool(true),S}\eqno \mbox{[True]}$$

$$\frac{}{so,S,E\vdash \mbox{false} : Bool(false),S}\eqno \mbox{[False]}$$

$$\frac{i\mbox{ is an integer constant}}{so,S,E\vdash i : Int(i),S}\eqno \mbox{[Int]}$$

$$\frac{\begin{array}{l} s\mbox{ is a string constant}\\ l ... ...d{array}}{so,S,E\vdash s : String(l,s),S}\eqno \mbox{[String]}$$

A new expression is more complicated than one might expect:

$$\frac{\begin{array}{l} T_0 = \left\{ \begin{array}{rl} X &... ...ray}}{so,S_1,E\vdash \mbox{new }T : v_1,S_3}\eqno \mbox{[New]}$$

The tricky thing in a new expression is to initialize the attributes in the right order. If an attribute does not have an initializer, do not evaluate an assignment expression for it in the final step. Note also that, during initialization, attributes are bound to the default of the appropriate class.

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : v_1,S_2\\ so,... ..._0.f(e_1,\ldots,e_n) : v_{n+1},S_{n+4}}\eqno \mbox{[Dispatch]}$$

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : v_1,S_2\\ so,... ..._1,\ldots,e_n) : v_{n+1},S_{n+4}}\eqno \mbox{[StaticDispatch]}$$

The two dispatch rules do what one would expect. The arguments are evaluated and saved. Next, the expression on the left-hand side of the ``.'' is evaluated. In a normal dispatch, the class of this expression is used to determine the method to invoke; otherwise the class is specified in the dispatch itself.

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Bool(true),S_2\... ..._2\mbox{ else }e_3\mbox { fi} : v_2,S_3}\eqno \mbox{[If-True]}$$

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Bool(false),S_2... ...2\mbox{ else }e_3\mbox { fi} : v_3,S_3}\eqno \mbox{[If-False]}$$

There are no surprises in the if-then-else rules. Note that value of the predicate is a Bool object, not a boolean.

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : v_1,S_2\\ so,... ...2;\ldots; e_n;\mbox{ \}} : v_n,S_{n+1}}\eqno \mbox{[Sequence]}$$

Blocks are evaluated from the first expression to the last expression, in order. The result is the result of the last expression.

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : v_1,S_2\\ l_1... ..._1\leftarrow e_1\mbox{ in } e_2 : v_2,S_{4}}\eqno \mbox{[Let]}$$

A let evaluates any initialization code, assigns the result to the variable at a fresh location, and evaluates the body of the let. (If there is no initialization, the variable is initialized to the default value of $T_1$.) We give the operational semantics only for the case of let with a single variable. The semantics of a multiple let

$$\rm let\ x_1 : T_1 \leftarrow e_1,\ x_2: T_2 \leftarrow e2, \ldots,\ x_n :T_n \leftarrow e_n\ in\ e\$$

is defined to be the same as

$$\rm let\ x_1 : T_1 \leftarrow e_1\ in\ (let\ x_2 :T_2 \leftarrow e_2,\ldots,\ x_n : T_n \leftarrow e_n\ in\ e\ )\$$

$$\frac{\begin{array}{l} so,S_1,E\vdash e_0 : v_0,S_2\\ v_0... ..._n\Rightarrow e_n;\mbox{ esac} : v_1,S_{4}}\eqno \mbox{[Case]}$$

Note that the case rule requires that the class hierarchy be available in some form at runtime, so that the correct branch of the case can be selected. This rule is otherwise straightforward.

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Bool(true),S_2\... ...{ loop } e_2\mbox{ pool} : void,S_{4}}\eqno \mbox{[Loop-True]}$$

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Bool(false),S_2... ... loop } e_2\mbox{ pool} : void,S_{2}}\eqno \mbox{[Loop-False]}$$

There are two rules for while: one for the case where the predicate is true and one for the case where the predicate is false. Both cases are straightforward. The two rules for isvoid are also straightforward:

$$\frac{so,S_1,E\vdash e_1 : void,S_2}{so,S_1,E\vdash \mbox {isvoid } e_1 : Bool(true),S_2}\eqno \mbox{[IsVoid-True]}$$

$$\frac{so,S_1,E\vdash e_1 : X(\ldots),S_2}{so,S_1,E\vdash \mbox {isvoid } e_1 : Bool(false),S_2}\eqno \mbox{[IsVoid-False]}$$

The remainder of the rules are for the primitive arithmetic and logical operations. These are all easy rules.

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Bool(b),S_2\\ ... ...y}}{so,S_1,E\vdash \mbox{not }e_1 : v_1,S_2}\eqno \mbox{[Not]}$$

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Int(i_1),S_2\\ ... ...y}}{so,S_1,E\vdash \mbox{\~{}}e_1 : v_1,S_2}\eqno \mbox{[Neg]}$$

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Int(i_1),S_2\\ ... ...y}}{so,S_1,E\vdash e_1\ op\ e_2 : v_1,S_3}\eqno \mbox{[Arith]}$$

Cool Ints are 32-bit two's complement signed integers; the arithmetic operations are defined accordingly.

The notation and rules given above are not powerful enough to describe how objects are tested for equality, or how runtime exceptions are handled. For these cases we resort to an English description.

In $e_1 = e_2$, first $e_1$ is evaluated and then $e_2$ is evaluated. The two objects are compared for equality by first comparing their pointers (addresses). If they are the same, the objects are equal. The value void is not equal to any object except itself. If the two objects are of type String, Bool, or Int, their respective contents are compared. < and <= are handled similarly. The case for integer arguments is simple:

$$\frac{\begin{array}{l} so,S_1,E\vdash e_1 : Int(i_1),S_2\\ ... ...ay}}{so,S_1,E\vdash e_1\ op\ e_2 : v_1,S_3}\eqno \mbox{[Comp]}$$

... but String and Bool also admit comparisons. String comparisons are performed using the standard ASCII string ordering (e.g., "abc" < "xyz"). For booleans, false is defined to be less than true. Any other comparison (e.g., a comparison among non-void objects of different types) returns false. Note that for some objects this may be unintuitive: if c is a Cat and d is a Dog then c < d is false but d < c is also false. Note also that comparison is based on the dynamic type of the object, not on the static type of the object.

In addition, the operational rules do not specify what happens in the event of a runtime error. When a runtime error occurs, output is flushed and execution aborts. The following list specifies all possible runtime errors.

1. A dispatch (static or dynamic) on void.
2. A case on void.
3. Execution of a case statement without a matching branch.
4. Division by zero.
5. Substring out of range. (This error is always reported on line 0, since it occurs inside an "internal" library function.)
6. Heap overflow. (You do not need to implement this runtime error.)
7. Stack overflow.

Each outstanding "method invocation" (static or dynamic) and each outstanding "new" object allocation expression counts as a "Cool Activation Record". (Just to be clear, that second clause about "new" is counting currently-resolving constructor calls, not "total objects living in the heap".) A Cool interpreter must flag a "stack overflow" runtime error if and only if there are 1000 (one thousand) or more outstanding Cool Activation Records.

Finally, the rules given above do not explain the execution behaviour for dispatches to primitive methods defined in the Object, IO, or String classes. Descriptions of these primitive methods are given in Sections 8.3-8.5.