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 the variable x \in \mathit{Var}, and for writing out the value of the arithmetic expression a \in \mathit{AExp} (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's and 1's 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 execute the program: while true do (x:=x+1; thread x:=x-1 end) from a state s such that s(x)=0.

* The third assignment consists of Exercises 4.13, 4.14 and 4.19 from the textbook. Please bring cleanly written and stapled solutions to the class on April 4, at the beginning of class.
* Exercise 4.13: Use CS to generate the abstract machine code for the statement z:=0; while y<=x do (z:=z+1; x:=x-y)and execute the resulting code from a state s such that s(x)=17 and s(y)=5.
* Exercise 4.14: Replace the while statement of the language While with the statement repeat S until b. Adapt CS for this statement (and potentially also the SOS for any new AML instruction that you might add). Hint: You could get inspiration from the equivalence established in Exercise 2.10, namely that repeat S until b is semantically equivalent to S; while ¬b do S.
* Exercise 4.19: Use structural induction on Boolean expressions to show that for all Boolean expressions b and states s, \left<\mathcal{CB}\!\left[\!\left[b\right]\!\right], \varepsilon, s\right> \triangleright^+\left<\varepsilon, \mathcal{B}\!\left[\!\left[b\right]\!\right](s), s\right>.

* The fourth assignment consists of exercises 5.18, 5.49, 5.51 and 5.53(c) from the textbook. Please bring cleanly written and stapled solutions to the class on April 247.
* Exercise 5.18: Show that (\mathcal{P}(A), \subseteq) is a complete lattice, where \mathcal{P}(A) denotes the set of all subsets of the set A. In other words, prove that every subset X of \mathcal{P}(A) has a least upper bound.
* Exercise 5.49: Compute the denotation of the statement z:=0; while y<=x do (z:=z+1; x:=x-y). For the while-loop you should compute the first few approximants of its denotation, guess the general shape of the i-th approximant, and find the denotation of the loop as the lub of the approximation sequence.
* Exercise 5.51: Let us replace the while statement of the language While with the statement repeat S until b. Define the denotation of the repeat statement as the least fixed point of a transformer. Hint: think of a semantic equivalence (corresponding to an unfolding of the repeat-loop) that you can use to present the denotation of the statement as the (least) solution to an equation.
* Exercise 5.53(c): Use the denotational semantics of While to show that while b do S is semantically equivalent to if b then (S; while b do S) else skip. Hint: Recall that this equivalence was used to derive the equation defining the denotation of the while construct! The proof should then be straightforward, using that the denotation of the loop is a fixed point of the functional F_{b,S}.