A simple fixpoint argument without the restriction to continuity

DOI10.1007/BF00268074zbMath0591.68007MaRDI QIDQ1075045

A. J. M. van Gasteren, Edsger W. Dijkstra

Publication date: 1986

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

programming language semanticsweakest preconditionfixpoint equationnoncontinuous predicate transformerstransfinite ordinalsunbounded nondeterminacy

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items

A fixpoint theory for non-monotonic parallelism ⋮ The weakest precondition calculus: Recursion and duality ⋮ A calculus of refinements for program derivations ⋮ Continuity in Semantic Theories of Programming ⋮ Properties of data flow frameworks: A unified model ⋮ Refinement concepts formalised in higher order logic ⋮ Constructive design of a hierarchy of semantics of a transition system by abstract interpretation

Cites Work

• Proving total correctness of nondeterministic programs in infinitary logic
• A lattice-theoretical fixpoint theorem and its applications
• A Weaker Precondition for Loops
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item