A Weaker Precondition for Loops

DOI10.1145/69622.357189zbMath0492.68014OpenAlexW2102484310MaRDI QIDQ3954796

H. J. Boom

Publication date: 1982

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/69622.357189

zbMATH Keywords

verificationoperational semanticsnondeterminismweakest preconditionfair schedulingtotal correctnesspredicate transformerAckermann's functionpre- and postconditionsunbounded nondeterminismfair do loop

Mathematics Subject Classification ID

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

Related Items (9)

While-programs with nondeterministic assignments and the logic ALNA ⋮ A calculus of refinements for program derivations ⋮ On the total correctness of nondeterministic programs ⋮ Proving total correctness of nondeterministic programs in infinitary logic ⋮ Data refinement of predicate transformers ⋮ Complete proof rules for strong fairness and strong extreme fairness ⋮ Alternating states for dual nondeterminism in imperative programming ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ A simple fixpoint argument without the restriction to continuity

This page was built for publication: A Weaker Precondition for Loops