G. Futschek:

"Algebraic Properties of Loop Invariants";

Lecture Notes in Computer Science,735(1993), 57 - 66.

A set P(DO, R) of all invariants that ensure termination and where the postcondition R is true after termination is defined for every loop DO and for every postcondition R. Complying with the corresponding properties required, these sets P(DO, R) induce a topology on wp(DO, R). The weakest precondition wp(DO, R) is the weakest invariant of DO with respect to R. The topology P(DO, R) has a non-trivial structure and contains arbitrary conjunctions of invariants.

http://dx.doi.org/10.1007/BFb0039700

Created from the Publication Database of the Vienna University of Technology.