next up previous contents
Next: Expr Up: Semantics Previous: Type Declarations   Contents


Evaluation Rules

The evaluation of a Vesta program corresponds to the abstract evaluation:

  Eval( M([]) , C-initial)

where M is the closure corresponding to the contents of an immutable file (a system model) in the Vesta repository and C-initial is an initial context. M's model should have the syntactic form defined by the nonterminal Model described in Section A.3.3.13 below. C-initial defines the names and associated values of the built-in primitive operators and functions described in Section A.3.4 below.

The definition of Eval by cases follows. Unless E is handled by one of these cases, Eval(E, C) yields a runtime error. As mentioned above, the domain of Eval includes the language generated by the concrete grammar as a proper subset. Thus, in some of the cases below, the expression E can arise only as an intermediate result of another case of Eval. These cases are explicitly noted.

The pseudo-code that defines the various cases of Eval and the primitive functions should be read like C++. That code assumes the declaration for the representation of Vesta values shown in Table A.2. Note that the operator== is the one invoked by uses of ``=='' in the C++ pseudo-code. It is not to be confused with the primitive equality operator defined on various Vesta types in Section A.3.4. The pseudo-code also refers to the constants shown in Table A.3.


Table A.2: A C++ class declaration for Vesta values.
\begin{table}{\small\begin{verbatim}class val {
public:
operator int();
// ...
...ame type and are equal, and
// false (0) otherwise
}\end{verbatim}}
\end{table}



Table A.3: Definitions of constants used by the pseudo-code.
\begin{table}{\small\begin{verbatim}static val true; // value of literal TRUE
...
...f literal [ ]
static val err; // value of literal ERR\end{verbatim}}
\end{table}


For convenience, the pseudo-code adopts the following notational conventions:

In each of the following sections, we first present the relevant portions of the language syntax. We then present the evaluation rules that apply to those syntactic constructs. The complete language syntax is given in Section A.4.



Subsections
next up previous contents
Next: Expr Up: Semantics Previous: Type Declarations   Contents
Allan Heydon, Roy Levin, Timothy Mann, Yuan Yu