Zeitschriftenartikel:
G. Futschek:
"Algebraic Properties of Loop Invariants";
Lecture Notes in Computer Science,
735
(1993),
S. 57
- 66.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/BFb0039700
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.