Nyhetsflöde

The requirement for the course is a pass on the assignments, the lab assignments, and the written exam. The grade will be the grade obtained at the written exam. You're allowed to bring the course book, hand-outs and own lecture notes taken in class.

Note that you must be registered for the course in order to have the result of your exam reported.

Grading The exam will be graded based on the intended learning outcomes of the course, classified in three levels. After the course, students will be able, among others, to (with approximate levels):

Level E: Basic Constructions
* Execute statements in:

* natural semantics, i.e. derive transitions
* structural operational semantics, i.e. construct the configuration space and draw the configuration graph
* abstract machine semantics, i.e. translate statements to abstract machine code and execute the code
* denotational semantics, i.e. compute denotations (for loop-free programs)
* Express language properties (such as language determinism) and program properties (such as program termination) in different semantics
* Specify program correctness in Hoare logic (axiomatic semantics) by means of a pre-condition and a post-condition
* Generate tests via symbolic execution (for a given coverage criterion)
* Verify programs via symbolic execution and weakest precondition computation
Level C: Extended Concepts and Simple Proofs
* Prove semantic equivalence of two statements:

* in natural semantics
* in denotational semantics
* Extend a given semantics to new language constructs
* Develop abstract domains for program analysis by abstract interpretation
* Suggest and justify program transformations, supported by a suitable program analysis
Level A: Advanced Reasoning and Proofs
* Compute denotations of statements with while loops
* Prove language and program properties
* Relate different semantics
* Other theoretical problems involving proofs, including problems from fixed-point theory
Bonus points will be taken into account, namely one bonus point per homework assignment handed in on time.

Exam resits Exam resits (sv. omtentor) are by mutual arrangement with the lecturer.

Previous Exams
* exam from 29 May 2017 (with partial solutions)
* exam from 3 June 2015 (with partial solutions)
* exam from 21 May 2013 (with partial solutions)
* exam from 26 May 2011 (with hand-written solutions)
* exam from 14 December 2009 (with solutions)

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 corrperfect solution. Late andor 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 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).

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 tex:\displaystyle b evaluates to the same truth value when evaluated on any two states that agree on the free variables occurring in tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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, tex:\displaystyle \stackrel{?z}{\Longrightarrow} and tex:\displaystyle \stackrel{!z}{\Longrightarrow}, the first signifying the input of integer tex:\displaystyle z from the keyboard, and the second the output of integer tex:\displaystyle z on the console. The original transitions tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle EState consisting of normal states tex:\displaystyle s and abnormal states tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle b and states tex:\displaystyle s,  tex:\displaystyle \left<\mathcal{CB}\!\left[\!\left[b\right]\!\right], \varepsilon, s\right> \triangleright^+\left<\varepsilon, \mathcal{B}\!\left[\!\left[b\right]\!\right](s), s\right>.

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 tex:\displaystyle b evaluates to the same truth value when evaluated on any two states that agree on the free variables occurring in tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle x \in \mathit{Var}, and for writing out the value of the arithmetic expression tex:\displaystyle 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, tex:\displaystyle \stackrel{?z}{\Longrightarrow} and tex:\displaystyle \stackrel{!z}{\Longrightarrow}, the first signifying the input of integer tex:\displaystyle z from the keyboard, and the second the output of integer tex:\displaystyle z on the console. The original transitions tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle EState consisting of normal states tex:\displaystyle s and abnormal states tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle b and states tex:\displaystyle s,  tex:\displaystyle \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 24.
* Exercise 5.18: Show that tex:\displaystyle (\mathcal{P}(A), \subseteq)  is a complete lattice, where tex:\displaystyle \mathcal{P}(A) denotes the set of all subsets of the set tex:\displaystyle A. In other words, prove that every subset tex:\displaystyle X of tex:\displaystyle \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 tex:\displaystyle F_{b,S}.

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 tex:\displaystyle b evaluates to the same truth value when evaluated on any two states that agree on the free variables occurring in tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle x \in \mathit{Var}, and for writing out the value of the arithmetic expression tex:\displaystyle 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, tex:\displaystyle \stackrel{?z}{\Longrightarrow} and tex:\displaystyle \stackrel{!z}{\Longrightarrow}, the first signifying the input of integer tex:\displaystyle z from the keyboard, and the second the output of integer tex:\displaystyle z on the console. The original transitions tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle EState consisting of normal states tex:\displaystyle s and abnormal states tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle b and states tex:\displaystyle s,  tex:\displaystyle \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 tex:\displaystyle (\mathcal{P}(A), \subseteq)  is a complete lattice, where tex:\displaystyle \mathcal{P}(A) denotes the set of all subsets of the set tex:\displaystyle A. In other words, prove that every subset tex:\displaystyle X of tex:\displaystyle \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 tex:\displaystyle F_{b,S}.

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 tex:\displaystyle b evaluates to the same truth value when evaluated on any two states that agree on the free variables occurring in tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle x \in \mathit{Var}, and for writing out the value of the arithmetic expression tex:\displaystyle 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, tex:\displaystyle \stackrel{?z}{\Longrightarrow} and tex:\displaystyle \stackrel{!z}{\Longrightarrow}, the first signifying the input of integer tex:\displaystyle z from the keyboard, and the second the output of integer tex:\displaystyle z on the console. The original transitions tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle EState consisting of normal states tex:\displaystyle s and abnormal states tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle b and states tex:\displaystyle s,  tex:\displaystyle \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 27.
* Exercise 5.18: Show that for any set tex:\displaystyle A, the partial order tex:\displaystyle (\mathcal{P}(A), \subseteq)  is a complete lattice, where tex:\displaystyle \mathcal{P}(A) denotes the set of all subsets of the set tex:\displaystyle A. In other words, prove that every subset tex:\displaystyle X of tex:\displaystyle \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 tex:\displaystyle F_{b,S}.

* The fifth assignment consists of one exploratory problem. Please bring cleanly written solutions to the (first) 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.

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 tex:\displaystyle b evaluates to the same truth value when evaluated on any two states that agree on the free variables occurring in tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle x \in \mathit{Var}, and for writing out the value of the arithmetic expression tex:\displaystyle 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, tex:\displaystyle \stackrel{?z}{\Longrightarrow} and tex:\displaystyle \stackrel{!z}{\Longrightarrow}, the first signifying the input of integer tex:\displaystyle z from the keyboard, and the second the output of integer tex:\displaystyle z on the console. The original transitions tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle EState consisting of normal states tex:\displaystyle s and abnormal states tex:\displaystyle \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 tex:\displaystyle s such that tex:\displaystyle 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 tex:\displaystyle s such that tex:\displaystyle s(x)=17 and tex:\displaystyle 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 tex:\displaystyle b and states tex:\displaystyle s,  tex:\displaystyle \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 27.
* Exercise 5.18: Show that for any set tex:\displaystyle A, the partial order tex:\displaystyle (\mathcal{P}(A), \subseteq)  is a complete lattice, where tex:\displaystyle \mathcal{P}(A) denotes the set of all subsets of the set tex:\displaystyle A. In other words, prove that every subset tex:\displaystyle X of tex:\displaystyle \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 tex:\displaystyle F_{b,S}.

* The fifth assignment consists of one exploratory problem. Please bring cleanly written solutions to the (first) 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 (first) 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  tex:\displaystyle P \Rightarrow Q \vee b  is not valid. Hint: formula  tex:\displaystyle P \Rightarrow Q \vee b  is a state property; for it not to be valid means that there is a state tex:\displaystyle s at which tex:\displaystyle P is true but tex:\displaystyle Q and tex:\displaystyle b are false.

There will be two laboratory assignments. These are to be carried out in teams of at most two, at home. The lab sessions are only for getting assistance and presenting the solutions (see instructions on the respective document). For each assignment there will be one dedicated help session and one reporting session. For the latter, please be on time and have your report printed and stapled, and a computer ready to execute your program.

* The first lab assignment is about implementing an interpreter for the While language based on the notion of abstract machines developed in Chapter 4 of the textbook. The help session for this lab is on April 7, while the reporting session is on April 25.
* The second lab assignment adapts the interpreter from the first one to run with abstract values instead of with concrete ones, thus implementing the abstract interpretation technique for program analysis developed in Chapter 7 of the textbook, but in an operational semantics style. The technique is applied to program transformation.
* An alternative option for the second lab assignment is to explore some popular static analysis tool. If you choose this option, please do the following:
* Select a popular static analysis tool that you can get hold of. Some of the best known ones are Coverity, Clocwork, FXCop, and the Clang Analyzer. Check also this list on Wikipedia.
* Install the tool on your machine. Make sure that it works properly by testing it on some examples.
* Send an e-mail to Dilian to get approval for your choice.
* Experiment with the tool. Find out what analyses the tool supports, and what technique is used for them (if this information can be found).
* Find the strengths and the limitations of the tool.
* Write a report that summarizes your findings about the tool:
* easiness of installation and use,
* supported checks and the underlying techniques,
* small own examples showing the strengths and limitations of the tool.

There will be two laboratory assignments. These are to be carried out in teams of at most two, at home. The lab sessions are only for getting assistance and presenting the solutions (see instructions on the respective document). For each assignment there will be one dedicated help session and one reporting session. For the latter, please be on time and have your report printed and stapled, and a computer ready to execute your program.

* The first lab assignment is about implementing an interpreter for the While language based on the notion of abstract machines developed in Chapter 4 of the textbook. The help session for this lab is on April 7, while the reporting session is on April 25.To report your lab assignment, please select a time slot from this Doodle.
* The second lab assignment adapts the interpreter from the first one to run with abstract values instead of with concrete ones, thus implementing the abstract interpretation technique for program analysis developed in Chapter 7 of the textbook, but in an operational semantics style. The technique is applied to program transformation.An alternative option for the second lab assignment is to explore some popular static analysis tool. If you choose this option, please do the following:
* Select a popular static analysis tool that you can get hold of. Some of the best known ones are Coverity, Clocwork, FXCop, and the Clang Analyzer. Check also this list on Wikipedia.
* Install the tool on your machine. Make sure that it works properly by testing it on some examples.
* Send an e-mail to Dilian to get approval for your choice.
* Experiment with the tool. Find out what analyses the tool supports, and what technique is used for them (if this information can be found).
* Find the strengths and the limitations of the tool.
* Write a report that summarizes your findings about the tool:
* easiness of installation and use,
* supported checks and the underlying techniques,
* small own examples showing the strengths and limitations of the tool.

There will be two laboratory assignments. These are to be carried out in teams of at most two, at home. The lab sessions are only for getting assistance and presenting the solutions (see instructions on the respective document). For each assignment there will be one dedicated help session and one reporting session. For the latter, please be on time and have your report printed and stapled, and a computer ready to execute your program.

* The first lab assignment is about implementing an interpreter for the While language based on the notion of abstract machines developed in Chapter 4 of the textbook. The help session for this lab is on April 7, while the reporting session is on April 25.To report your lab assignment, please select a time slot from this Doodle.
* The second lab assignment adapts the interpreter from the first one to run with abstract values instead of with concrete ones, thus implementing the abstract interpretation technique for program analysis developed in Chapter 7 of the textbook, but in an operational semantics style. The technique is applied to program transformation.An alternative option for the second lab assignment is to explore some popular static analysis tool. If you choose this option, please do the following:
* Select a popular static analysis tool that you can get hold of. Some of the best known ones are Coverity, Clocwork, FXCop, and the Clang Analyzer. Check also this list on Wikipedia.
* Install the tool on your machine. Make sure that it works properly by testing it on some examples.
* Send an e-mail to Dilian to get approval for your choice.
* Experiment with the tool. Find out what analyses the tool supports, and what technique is used for them (if this information can be found).
* Find the strengths and the limitations of the tool.
* Write a report that summarizes your findings about the tool:
* easiness of installation and use,
* supported checks and the underlying techniques,
* small own examples showing the strengths and limitations of the tool.

There will be two laboratory assignments. These are to be carried out in teams of at most two, at home. The lab sessions are only for getting assistance and presenting the solutions (see instructions on the respective document). For each assignment there will be one dedicated help session and one reporting session. For the latter, please be on time and have your report printed and stapled, and a computer ready to execute your program.

* The first lab assignment is about implementing an interpreter for the While language based on the notion of abstract machines developed in Chapter 4 of the textbook. The help session for this lab is on April 7, while the reporting session is on April 25.To report your lab assignment, please select a time slot from this Doodle.
* The second lab assignment adapts the interpreter from the first one to run with abstract values instead of with concrete ones, thus implementing the abstract interpretation technique for program analysis developed in Chapter 7 of the textbook, but in an operational semantics style. The technique is applied to program transformation. We decided to move the help session for this lab to May 9, and the reporting session to May 16.An alternative option for the second lab assignment is to explore some popular static analysis tool. If you choose this option, please do the following:
* Select a popular static analysis tool that you can get hold of. Some of the best known ones are Coverity, Clocwork, FXCop, and the Clang Analyzer. Check also this list on Wikipedia.
* Install the tool on your machine. Make sure that it works properly by testing it on some examples.
* Send an e-mail to Dilian to get approval for your choice.
* Experiment with the tool. Find out what analyses the tool supports, and what technique is used for them (if this information can be found).
* Find the strengths and the limitations of the tool.
* Write a report that summarizes your findings about the tool:
* easiness of installation and use,
* supported checks and the underlying techniques,
* small own examples showing the strengths and limitations of the tool.

There will be two laboratory assignments. These are to be carried out in teams of at most two, at home. The lab sessions are only for getting assistance and presenting the solutions (see instructions on the respective document). For each assignment there will be one dedicated help session and one reporting session. For the latter, please be on time and have your report printed and stapled, and a computer ready to execute your program.

* The first lab assignment is about implementing an interpreter for the While language based on the notion of abstract machines developed in Chapter 4 of the textbook. The help session for this lab is on April 7, while the reporting session is on April 25.To report your lab assignment, please select a time slot from this Doodle.
* The second lab assignment adapts the interpreter from the first one to run with abstract values instead of with concrete ones, thus implementing the abstract interpretation technique for program analysis developed in Chapter 7 of the textbook, but in an operational semantics style. The technique is applied to program transformation. The help session for this lab is on May 9, while the reporting session is on May 16.To report your second lab assignment, please select a time slot from this Doodle.An alternative option for the second lab assignment is to explore some popular static analysis tool. If you choose this option, please do the following:
* Select a popular static analysis tool that you can get hold of. Some of the best known ones are Coverity, Clocwork, FXCop, and the Clang Analyzer. Check also this list on Wikipedia.
* Install the tool on your machine. Make sure that it works properly by testing it on some examples.
* Send an e-mail to Dilian to get approval for your choice.
* Experiment with the tool. Find out what analyses the tool supports, and what technique is used for them (if this information can be found).
* Find the strengths and the limitations of the tool.
* Write a report that summarizes your findings about the tool:
* easiness of installation and use,
* supported checks and the underlying techniques,
* small own examples showing the strengths and limitations of the tool.

Book cover

Nielson and Nielson Semantics with Applications: An Appetizer Springer-Verlag, 2007, ISBN: 978-1-84628-691-9 Available from Kårbokhandeln at the start of the period. In addition: some hand-written slides on axiomatic semantics and verification condition generation (see outline, part III), and a text explaining the principle of structural induction.

Here are my own LaTeX definitions. Derivation trees I create with the following package. Additional reading for the curious student:

* a paper by Freund and Mitchell formalizing the Java Virtual Machine and Language, thus providing an abstract machine semantics for the Java bytecode language JVML.