Formal Methods, form09

Assignments

There will be four mandatory homework assignments. These will be peer-assessed in class and then collected by the lecturer. Assignments that are handed in on time and that are of acceptable quality will give bonus points for the final exam.

Assignment 1

Due in class on February 2, 2009. Consists of three problems:

Problem 1. (Exercises 4.3, problem 13) Verify the following program Copy1:

     a = x;
     y = 0;
     while (a != 0) {
          y = y + 1;
          a = a -1;
          }   

for precondition  x =>  0  and postcondition  x = y . Present the proof as a proof tableau. Clearly identify and justify the resulting proof obligations.

Problem 2. Specify and verify the second factorial program Fac2:

     y = 1;
     while (x != 0) {
          y = y * x;
          x = x - 1;
          }

Present the proof as a proof tableau. Clearly identify and justify the resulting proof obligations.

Problem 3. (Exercises 4.3, problem 20) Let all while-statements while (B) {C} in program P be annotated with invariant candidates eta at the end of their body, and with eta /\ B at the beginning of their body. Describe how a proof of partial correctness of  (| phi |) P (| psi |)  can be automatically reduced to showing the validity of some assertion  psi_1 /\ psi_2 /\ ... /\ psi_n . Ideally, provide the pseudo-code of an algorithm. Exemplify your proposal on an interesting example, for instance on an while-annotated version of Fac2 so that you can compare with your proof by hand.

Assignment 2

Due in class on February 16, 2009. Consists of two problems:

Problem 1.  Consider the following program for computing the greatest common divisor gcd(m, n) of two positive integers m and n:

     while (x != y) {
          while (x < y) {
               y = y - x;
               };
          while (y < x) {
               x = x - y;
               }
          }
              
Specify the program by means of a pre- and post-condition (the specification should meaningfully express the purpose of the program without knowing its text). Verify that the program meets its specification w.r.t. total correctness. Present the proof as a proof tableau. Clearly identify the invariant and the variant of the while loops. Identify and justify the resulting proof obligations. Hint: Use the notation gcd(x,y) in assertions. You will have to refer to certain properties of gcd in order to discharge some of the proof obligations.

Problem 2. Consider the following parallel program:

     z = 0;
     cobegin
          z = z + x;
     ||   z = z + y;
     coend

Prove partial correctness of the program w.r.t. precondition  x => 0 /\ y => 0  and postcondition  z => max(x,y)  by using the Owicki-Gries proof rule. Give a full proof of non-interference.

Assignment 3

Due in class on February 23, 2009. Consists of two problems: Exercise 1 and Exercise 3 from the LTL Exercises.

Assignment 4

Due in class on March 2, 2009. Consists of Exercise 6 from the LTL Exercises.