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>\).
- Exercise 4.13: Use CS to generate the abstract machine code for the statement
- 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 27.
- Exercise 5.18: Show that for any set \(A\), the partial order \((\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}\).
- The fifth assignment consists of one exploratory problem. Please bring cleanly written solutions to the class on April 27.
- 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 and stapled solutions to the class on May 2.
- 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 and proof.
- Verify the program. Present the proof (preferably) as a proof tableau/outline (that is, as a fully annotated program).
- Identify and justify the resulting proof obligations (aka verification conditions).
- 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 \Rightarrow Q \vee b\) is not valid.
Hint: formula \(P \Rightarrow Q \vee b\) is a state property; for it not to be valid means that there is a state \(s\) at which \(P\) is true but \(Q\) and \(b\) are false.
- Problem 1: Consider the following program implementing Euclid's algorithm for computing the greatest common divisor gcd(m,n) of two positive integers: