
























In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments: an invariant, for functional properties (ignoring termination); and a variant, for termination (ignoring functional properties). A single and simple definition is possible, removing this split. A loop is just the limit (a variant of the reflexive transitive closure) of a Noetherian (well-founded) relation. To prove the loop correct there is no need to devise an invariant and a variant; it suffices to identify the relation, yielding both partial correctness and termination. The present note develops the (small) theory and applies it to standard loop examples and proofs of their correctness.
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。