Automatische Erzeugung von Verifikations- und Falsifikationsbedingungen

Preprint series: 99-08, Reports on Computer Science

MSC:
68T20 Problem solving
03F03 Proof theory, general
CR: D.2.4.

Abstract: Abstract (Zusammenfassung):
The aim of program verification is to prove the correctness of a program
S with respect to a formal specification, that consists of a pre- and a
postcondition V and N. In other words: are program S and specification
(V, N) consistent?
-- V
S
-- N
Program S is correct, if S starts in a state that fulfills V and
terminates in state that fulfills N. The formal definition of
correctness is
S is correct wrt. (V, N) if [V => wp(S, N)].
wp(S, N) is the weakest precondition, that guarantees termination in a
state fulfilling N.
For the purpose of program verification the axiomatic or relational
semantics is necessary. These two kinds of formal semantics are
equivalent. Axiomatic semantics uses the wp-function, that works on the
complete lattice of predicates. Relational semantics uses the LP
(largest preset)-function, that works on the complete lattice of state
sets. These two lattices are isomorph thru the characteristic predicate
function of a set.
In order to work efficiently with the wp-function some properties of
that function are necessary and useful. Two new properties are shown:
strong disjunctivity for comparable predicates and the substitution
lemma for wp. Furthermore it turns out, that all properties of the
wp-function are easily provable in the lattice of state sets with
elementary set theory. A VC is defined to be a condition that implies
correctness, formally
[VC => [V => wp(S, N)].
A distinction is made between exact and approximate VCs.
The major results of the thesis are verifying loops without an invariant
and falsification conditions. In order to verify loops without a given
invariant, two strategies are possible:
1. generate the invariant or
2. compute the wp-function for the loop
Strategy 1 is used to compute invariants for for-loops. The invariant is
generated by substituting a constant in the postcondition by a variable,
more exactly the upper limit of the loop is substituted by the loop
variable. In general the upper limit is not a variable. Therefore the
loop is transformed into a semantically equivalent loop.
Strategy 2 is used to compute the wp of while-loops by a new method that
uses E-unification.
Falsification conditions (FCs) are very useful in practical program
verification. They explicitly prove the incorrectness of a program and
facilitate a localization of program errors. FCs are defined in an
analog way as VCs: an FC implies the incorrectness of a program,
formally
[FC => not [V => wp(S, N)].
FCs are reduced to constraint programming problems (cpp) or, in the case
of integer types, to integer programming problems (ipp). ipp also arise
in data dependence analysis. Therefore similar methods can be applied.

Keywords: program verification, relational semantics,