Publications in Scientific Journals:

G. Futschek:
"Algebraic Properties of Loop Invariants";
Lecture Notes in Computer Science, 735 (1993), 57 - 66.

English abstract:
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.

"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)

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