Predicate Transformers for Recursive Procedures with Local Variables
Copyright policy )Predicate Transformers for Recursive Procedures with Local Variables
Abstract. The weakest precondition semantics of recursive procedures with local variables are developed for an imperative language with demonic and angelic operators for unbounded nondeterminate choice. This does not require stacking of local variables. The formalism serves as a foundation for a proof rule for total correctness of (mutually) recursive procedures with local variables. This rule is illustrated by a simple example. Its soundness is proved for arbitrary well-founded variant functions.
- University of Groningen Netherlands
Frames, Proof rule, Semantics in the theory of computing, precondition semantics of recursive procedures, imperative language, Recursive procedures, Predicate transformers
Frames, Proof rule, Semantics in the theory of computing, precondition semantics of recursive procedures, imperative language, Recursive procedures, Predicate transformers
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).5 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!