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 correct solution. Late and 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 31 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 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 solutions to the class on April 14 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 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, =?z=> and =!z=>\stackrel{?z}{\Longrightarrow} and \stackrel{!z}{\Longrightarrow}, the first signifying the input of numbinteger z from the keyboard, and the second the output of numbinteger 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 termination.

* To distinguish between normal and abnormal termination, we introduce the set of extended states EState consisting of normal states s and abnormal states ŝ (s hat, \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. Note 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.

* Based on the structural operational semantics of the parallel construct par presented in the book (see page 52), capture the semantics of the new statement.
* 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.

* The third assignment consists of exercises 4.13, 4.14 and 4.19 from the textbook. Please bring cleanly written solutions to the class on April 14 at the beginning of class.
* Exercise 4.13: Use CS to generate abstract machine code for the statement z:=0; while y<=x do (z:=z+1; x:=x-y), and execute this statement from a state s such that s(x)=17 and s(y)=5.
* Exercise 4.14: Let us replace the while statement of the language While with the statement repeat S until b. Adapt CS for this statement. 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, <CB[[b]], epsilon, s> |>+ <epsilon, B[[b]](s), s>.

* The fourth assignment consists of exercises 5.18, 5.49, 5.51 and 5.53(c) from the textbook. Please bring cleanly written solutions to the (first) class on April 28.
* Exercise 5.18: Show that (P(A),subset) is a complete lattice, i.e. that every subset X of P(A) has a least upper bound (where P(A) denotes the set of all subsets of set A).
* Exercise 5.49: Compute iteratively the denotation of the statement z:=0; while y<=x do (z:=z+1; x:=x-y). That is, for the while loop, compute the first few approximants of the denotation, guess the general shape of the i-th approximant, and find the denotation as the lub of the sequence. Hint: similar to Example 5.48.
* 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 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: Note 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 corresponding transformer.

* The fifth assignment consists of one exploratory problem. Please bring cleanly written solutions to the (first) class on April 28.
* Problem: Develop an abstract structural operational semantics for a constant propagation analysis. The point of this analysis is to identify arithmetic and boolean expressions that will always evaluate to one and the same value, regardless of the state from which program execution starts (see Exercise 7.9 on page 160).

* Define the abstract domains, abstract operations, abstract semantic functions for the evaluation of arithmetic and boolean expressions, and abstract SOS rules for statements.
* Use your abstract semantics to support interesting program transformations. Provide at least one example program involving a while loop that can be simplified significantly. Be careful how you arrange the construction of the configuration graph in order to guarantee precision and termination of the construction! For example, you can use acceleration in order to guarantee termination, and use a prime values based execution in order to improve the precision of the analysis.

* The sixth (and last) assignment consists of three problems, not from the textbook. Please bring cleanly written solutions to the (first) class on May 5.
* Problem 1: Consider the following program implementing Euclid''s algorithm for computing the greatest common divisor gcd(m,n) of two positive integers: while ¬(x=y) do if x<=y then y:=y-x else x:=x-y.

* Specify the program by means of a pre- and a post-condition. The specification should meaningfully express the purpose of the program without knowing its implementation (i.e. from a user''s view). You can use the notation gcd(m,n) in your specification.
* Verify the program. Present the proof as a proof tableau/outline (that is, as a fully annotated program).
* Identify and justify the resulting proof obligations.
* Problem 2: Let us replace the while statement of the language While with the statement repeat S until b. Adapt the axiomatic semantics of the resulting language by providing a rule capturing the meaning of the repeat statement. Give an intuitive justification for your rule.
* Problem 3: Argue that a Hoare triple of shape {P} while b do S {Q} cannot be semantically valid if the formula P => b \/ Q is not valid. Hint: formula P => b \/ Q is a state property; for it not to be valid means that there is a state s where P is true but b and Q are false.