Predicate-Transformer Semantics of General Recursion

Research output: Contribution to journalArticleAcademicpeer-review

9 Citations (Scopus)
292 Downloads (Pure)

Abstract

We develop the semantics of a language with arbitrary atomic statements, unbounded nondeterminacy, and mutual recursion. The semantics is expressed in weakest preconditions and weakest liberal preconditions. Individual states are not mentioned. The predicates on the state space are treated as elements of a distributive lattice. The semantics of recursion is constructed by means of the theorem of Knaster-Tarski. It is proved that the law of the excluded miracle can be preserved, if that is wanted. The universal conjunctivity of the weakest liberal precondition, and the connection between the weakest precondition and the weakest liberal precondition are proved to remain valid. Finally we treat Hoare-triple methods for proving correctness and conditional correctness of programs.
Original languageEnglish
Pages (from-to)309-332
Number of pages24
JournalActa informatica
Volume26
Issue number4
Publication statusPublished - 1989

Fingerprint

Dive into the research topics of 'Predicate-Transformer Semantics of General Recursion'. Together they form a unique fingerprint.

Cite this