Specification

Values

Value Specification for LET

• ExpVal = Int + Bool
• DenVal = Int + Bool
• ExpVal = DenVal

Interface for values in LET

Constructors

• num-val : Int → ExpVal
• bool-val : Bool → ExpVal

Extractors

• expval→num : ExpVal → Int
• expval→bool : ExpVal → Bool

Environments

If we are going to evaluate expressions containing variables, we will need to know the value associated with each variable. We do this by keeping those values in an environment.

• ρ ranges over environments.
• [] denotes the empty environment.
• [*var* = *val*]ρ denotes (extend-env *var val* ρ).
• [*var*1 = *val*1, *var*2 = *val*2]ρ abbreviates [*var*1 = *val*1]([*var*2 = *val*2]ρ), etc.
• [*var*1 = *val*1, *var*2 = *val*2, ...] denotes the environment in which the value of *var*1 is *val*1, etc.

Expressions

Interface for Expressions

The value of a constant expression in any environment is the constant value. The value of a variable reference in an environment is determined by looking up the variable in the environment. The value of a difference expression in some environment is the difference between the value of the first operand in that environment and the value of the second operand in that environment. Of course, to be precise we have to make sure that the values of the operands are numbers, and we have to make sure that value of the result is a number represented as an expressed value.

Constructors

• const-exp : Int → Exp
• zero?-exp : Exp → Exp
• if-exp : Exp × Exp × Exp → Exp
• diff-exp : Exp × Exp → Exp
• var-exp : Var → Exp
• let-exp : Var × Exp × Exp → Exp

Observers

• value-of-program : Program → ExpVal
• value-of : Exp × Env → ExpVal

Grammar Specification for Expressions

Expression ::= Number
					 ::= Identifier
					 ::= zero? (Expression)
					 ::= if Expression then Expression else Expression
					 ::= - (Expression, Expression)
					 ...
					 ::= Program

Behavior for programs: a-program

In our language, a whole program is just an expression. In order to find the value of such an expression, we need to specify the values of the free variables in the program. So the value of a program is just the value of that expression in a suitable initial environment.

; #############################
; Equational Specification
; #############################

(value-of-program exp) = (value-of exp [i=[1], v=[5], x=[10])