by **
Stefan Kauer**

**Preprint series:**
99-08, Reports on Computer Science

**MSC:**- 68T20 Problem solving
- 03F03 Proof theory, general

**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,*

**Upload:** 1999-02-16

**Update:** 1999-02-16

The author(s) agree, that this abstract may be stored as full text and distributed as such by abstracting services.