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.
Background:
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
(provide
;; the core language definition:
simple-lang
;; the language extended with statement and expression contexts:
sl+c
;; the reduction relation
->simple-lang
;; 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
(reduction-relation
sl+c
[==> (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)))
"add"]
[==> (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 ...)
"ref"]
[==> (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 ...)
"set"]
[==> (block ((x n) ...) void s ...)
(block ((x n) ...) s ...)
"skip"]
[==> (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 ...)
"merge"]
with
[(--> (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")
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.
Deliverable:
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.