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.

* 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 13:15.
* 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).