G7400 F'12
Set 1
Set 2
Set 3
Set 4
Set 5
Set 6
Set 7
Set 8
Set 9
Set 10

Problem Set 5: Calculational Semantics for Imperative Languages

Due date: 10/12 @ at the beginning of class

Purpose: The goal of this problem set is to develop a "calculational" model of the semantics of a (simplified variant of) simple-lang. The solution will show that an imperative language has a naturally parallel semantics. Successful completion of the problem set will deepen your understanding of scope and ordering of assignment statements.


The module 5-provided.rkt provides some language definitions, sample programs, and a faulty attempt to specify a "calculational" semantics for a small imperative language:

  #lang racket 

    ;; the core language definition:
    ;; the language extended with statement and expression contexts:
    ;; the reduction relation
    ;; the examples: 
    s1 s2 s3 s4 s5)

  ;; -----------------------------------------------------------------------------

  (require redex)

  (define-language simple-lang 
    (s (x = e) (block (d ...) s ...) void)
    (e x n (+ e e))
    (d (x n))
    (n number)
    (x variable-not-otherwise-mentioned))

  (define s1 
    (term (block ((x 0) (y 1)) (x = (+ x 1)) (y = x))))

  (define s2 
    (term (block ((x 8) (y 9)) (x = 0) (block ((z 9)) (x = 0) (z = 2)) (y = 1))))

  (define s3
    (term (block ((x 0)) (block ((x 9)) (x = (+ x 1))))))

  (define s4
    (term (block ((x 0)) (block ((y 9)) (block ((z 3)) (y = x))))))

  (define s5
    (term (block ((x 0)) (x = 1) (x = (+ x 1)))))

  (for/and ((an-s (list s3 s1 s4 s2)))
    (redex-match? simple-lang s an-s))

  ;; -----------------------------------------------------------------------------

  (define-extended-language sl+c simple-lang
    (S hole (block (d ...) s ... S s ...) (x = E))
    (E hole (+ e E) (+ E e)))

  (define ->simple-lang
     [==> (block (d_1 ... (x n) d_2 ...) s_1 ... (in-hole S (+ n_1 n_2)) s_2 ...)
	  (block (d_1 ... (x n) d_2 ...) s_1 ... (in-hole S n_3) s_2 ...)
	  (where n_3 ,(+ (term n_1) (term n_2)))
     [==> (block (d_1 ... (x n) d_2 ...) s_1 ... (in-hole S x) s_2 ...)
	  (block (d_1 ... (x n) d_2 ...) s_1 ... (in-hole S n) s_2 ...)
     [==> (block (d_1 ... (x n) d_2 ...) s_1 ... (in-hole S (x = n_u)) s_2 ...)
	  (block (d_1 ... (x n_u) d_2 ...) s_1 ... (in-hole S void) s_2 ...)
     [==> (block ((x n) ...) void s ...)
	  (block ((x n) ...) s ...)
     [==> (block ((x_1 n_1) ...) (block ((x_2 n_2) ...) s_2 ...) s_1 ...)
	  (block ((x_1 n_1) ... (x_2 n_2) ...) s_2 ... s_1 ...)
     [(--> (in-hole S s_red) (in-hole S s_con))
      (==> s_red s_con)]))
The key change to simple-lang is that all variables are -- in C/C++-like fashion -- initialized, an action distinct from assignment statements (as you should know from C++).

The goal of the relation is to reduce programs to the shape

  (block ((x n) ...))
The primary mechanism is to understand an assignment statement as a tool for changing the declared value of a variable and to understand a reference to a variable inside of an expression as an instruction to look up its declared value. While the first three rules express these "sentiments", the last two rules simplify the programs so that the final result is readable. Sadly, the relation is also wrong.

Your solution file starts with

  #lang racket

  (require redex "5-provided.rkt")
The second line imports the pieces provided by 5-provided.rkt.

Problem 1:

Formulate test cases that specify all possible outcomes for the five provided sample programs.

Problem 2:

Use your understanding of C/Java-style programming to formulate the expected results for the five provided sample programs.

Formulate five test cases from the five sample programs and the five corresponding sample outcomes. Create a Racket function that consumes a reduction relation and abstracts over this test suite.

Run the function on the provided reduction relation. This should signal some test failures because the relation is faulty.

Problem 3:

Copy the reduction provided relation from 5-provided.rkt into your solution file and rename it ->simple-lang.v2.

Edit and/or supplement the ==> rules (and only those) of ->simple-lang.v2 with side conditions as needed so that they get triggered only according to your understanding of C's and Java's semantics. You must make side-conditions minimally stringent, i.e., any side conditions should not restrict the trigger conditions more than necessary. In the end, the reduction relation must pass your abstracted test suite from problem 2.

Hint The point of problem 1 is of course to reflect on the problems with the existing relation.

Problem 4:

Create the smallest possible example that shows -- via a traces expression --- how even the correct reduction relation can produce the single result of a program via multiple paths.


Send in a single Racket file. Its name should consist of the two last names in alphabetical order separated with a hyphen; its suffix must be .rkt.

Your file must start with the following two lines:

  ;; NameOfPartner1, NameOfPartner2 
  ;; email@of.partner1.com, email@of.partner2.com
appropriately instantiated of course. Also separate problems with lines of the shape ";; " followed by 77 "-". That gives you a width of 80 chars. Try to stick to this width for all of your code; it ensures basic readability.

last updated on Wed Nov 7 10:09:15 EST 2012generated with Racket