Assignments

There will be six written homework assignments (see below as they are published successively) as a mandatory part of passing HEM1. These will typically consist of a number of exercises taken from the textbook or composed by the course leader. The written solutions will be checked in class by peer reviewing, with the help of solutions provided by the course leader, and will then be collected. Each peer reviewed and passed assignment will give a bonus point for the final exam (out of 30 points). Note that participation in the peer review is a prerequisite for obtaining bonus points, since the review sessions are used to teach students to discuss alternative solutions and to read other students solutions. The criterion for passing is to have made a decent attempt to solve the problem rather than to have necessarily produced a perfect solution. Late or failed assignments need to be completed and sent to the course leader at a later occasion. There is no penalty for that, but also no bonus point.

* The first assignment consists of exercises 1.13, 2.3 and 2.7 from the textbook. Please bring cleanly written and stapled solutions to the class on March 27 at the beginning of class.
* Exercise 1.13: Use structural induction to show that a Boolean expression b evaluates to the same truth value when evaluated on any two states that agree on the free variables occurring in b.
* Exercise 2.3: Consider the statement: z:=0; while y<=x do (z:=z+1; x:=x-y). Construct a derivation tree w.r.t the natural semantics of While for this statement when executed from a state s such that s(x)=17 and s(y)=5.
* Exercise 2.7: Let us replace the while statement of the language While with the statement repeat S until b. Adapt the natural semantics with rules capturing the meaning of this statement. Show that: repeat S until b is semantically equivalent to: S; if b then skip else (repeat S until b).

* The second assignment consists of three problems (not from the textbook). Please bring cleanly written and stapled solutions to the class on April 4, at the beginning of class.
* Problem 1: Let us extend While with statements read x and write a, for reading in a value from the keyboard and storing it in variable x, and for writing out the value of expression a (in the current state) to the console, respectively.

* Complete the structural operational semantics for the resulting language. To capture interaction with the environment, one can introduce two new types of transitions between configurations, \stackrel{?z}{\Longrightarrow} and \stackrel{!z}{\Longrightarrow}, the first signifying the input of integer z from the keyboard, and the second the output of integer z on the console. The original transitions \Rightarrow remain, signifying "silent" transitions not involving interaction with the environment.
* Explore the configuration space of the program while true do (read x; write 1-x) from a state s such that s(x)=0, assuming only 0 and 1 are entered from the keyboard. Draw the configuration graph, as symmetrically as possible.
* Problem 2: Consider the language While extended with the abort statement causing abnormal (or exceptional) termination.

* To distinguish between normal and abnormal termination, we introduce the set of extended states EState consisting of normal states s and abnormal states \hat{s} (the convention being that the two agree on the values they assign to variables).
* Extend the natural semantics of the language by providing rules for abnormal termination. Notice that the rules for normal termination can stay unchanged!
* Use your semantics to execute the program: x:=2; while 0<=x do if x=1 then x:=2; (abort; x:=0) else x:=x-1 from an arbitrary state s.
* Is the language still deterministic? Justify your answer.
* Problem 3: Let us extend While with threads by adding the statement thread S end. The intended behaviour of this statement is that it generates a new thread executing statement S in parallel with the already existing threads.

* Extend the structural operational semantics of While to capture the semantics of the new statement, for instance by relying on the the parallel construct par and its semantics as presented in the book (see page 52). Is it problematic? Why? Can you suggest some better treatment?
* Use your semantics to describe an execution of the program while true do (x:=x+1; thread x:=x-1 end) from a state s such that s(x)=0.