You are here: Home [Varies] Predicates and Prejudice - Proving Correctness of Programs

# Predicates and Prejudice - Proving Correctness of Programs

Course type B. Sc. Project, M.Sc. Praktikum,  M.Sc. Teamproject Matthias Heizmann Depending on course type

## Predicates

In which of the following procedures does the assert statement never fail? Why?

• We can prove that the assertion in the procedure raven never fails by showing that the predicate y==x is a loop invariant of the while loop.
• We can prove that the assertion in the procedure blackbird never fails by showing that the predicates x>=0 and y==0 are loop invariants of the while loop.

Given these predicates, the correctness of the procedures can easily be shown using a technique called predicate abstraction. The question is: how do we guess the right predicates?

## Prejudice

• It is said that every German loves football. However this is not true, I know some Germans that don't like football at all. But if you meet some German the chance is high that he or she likes football.
• It is said that it is always raining in Scotland. However this is not true. But there are regions in Scotland where the risk of rain is much higher than in Freiburg.

## Predicates and Prejudice

• If a procedure contains the statement y:=x then the predicate y==x is useful in a correctness proof. Of course this is not always true, the procedure blackbird is a counterexample. But for some procedures the predicate y==x is a good guess.
• If a procedure contains the statement x:=0 and the statement x:=x+1 then the predicate x>=0 is useful in a correctness proof. Of course this is not always true, the procedure raven is a counterexample. But for some procedures the predicate x>=0 is a good guess.