EXERCISE 1 (STATIC AND DYNAMIC SEMANTICS FOR A STACK-VARIABLE LANGUAGE)
Consider the following stack-variable language, SVL:
- -) The syntax of a SVL program is given by the syntactic category, P
(which is in turn defined in terms of SVL expressions as given by the syntactic category, E):
P : (run E) // evaluate expression E (with an initially empty stack)
E : con n // push constant integer n onto the stack (n natural number)
| inc n // increase top element on stack by constant n (n natural number)
| dec n // decrease top element on stack by constant n (n natural number)
| neg // integer negatation: invert the sign of the top element on the stack
| get x // push value of x onto stack (implicitly 0 if x has never been assigned)
| put x // pop top element from stack and assign it to variable x
| (ifnz E else E') // pop top element from stack, evaluate E if it was non-zero (E', if not)
| (whnz E) // pop top element from stack, evaluate E if it was non-zero...
// ...after evaluation of E, reevaluate the whole expression: "whnz E"
| (seq E ; E') // sequential evaluation: evaluate E, then evaluate E'
- a) Write an SVL program P that adds the values held in the variables x and y.
- b1) Give the signatures (for all relations you plan to use in assignment "b2" below):
- b2) Give a reasonable static semantics for the SVL language, making sure that:
- -) for all P programs (run E), the evaluation of E starting with the empty stack always results in a stack of height 1 (for "the result");
- -) for all P programs, inc, neg, get, ifnz-else, and whnz are never executed with a
stack height of less than one (for popping the top element on the stack); and
- -) branching along either control-flow path of the ifnz-else-construction (i.e. evaluating either E or E')
always produces the same resulting stack height.
- -) figure out a reasonable static requirement for the whnz-construction.
[ Hint: You may, for instance, use (possibly among other things) an expression well-formedness relation,
|-wfe, relating an expression, E, an assumed initial stack height, n, and a
resulting stack height, m (e.g., "|-wfe E:n:m") ]
- c1) Give the configurations, terminal configurations, and signature of the transition relation (for all transition systems you plan to use in assignment "c2" below).
Also, in case you are using any intermediate syntax, introduce it explicitly by giving the new grammar for P and E with the intermediate syntax added
(if you are using any).
- c2) Give a reasonable small-step structural operational dynamic semantics for the SVL language as informally
described (in gray color) above.
-
[ Hint: For configurations, you may wish to use (possibly among other things) <M,E,W>
(where M is a memory, E is an expression, and W (omega) is an integer sequence (stack) belonging to Z* ]
[ Hint': Also, you may wish to use the syntactic conventions that "ε" (epsilon) describes
the empty integer sequence (empty stack), and "n::w" describes the concatenation of integer n
and integer sequence W (omega) ]
| [ 30% ] |
