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)
http://dx.doi.org/10.1007/BFb0039700
Created from the Publication Database of the Vienna University of Technology.