A Weaker Precondition for Loops

DOI10.1145/69622.357189MaRDI QIDQ3954796zbMATH OpenOpenAlexFDO

Authors 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

verificationnondeterminismweakest preconditionoperational semanticsfair schedulingtotal correctnesspredicate transformerAckermann's functionpre- and postconditionsunbounded nondeterminismfair do loop

Mathematics Subject Classification ID

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

Cited in

(9)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3954796)