[Zurück]


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.