# Formal Methods, form09

DD2452 Formal Methods: Labs
## 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.