A simple fixpoint argument without the restriction to continuity

DOI10.1007/BF00268074MaRDI QIDQ1075045zbMATH OpenFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 3949704
• scientific article; zbMATH DE number 4188755
• scientific article; zbMATH DE number 1001932
• scientific article; zbMATH DE number 5120984
• The fixed point property for continua
• scientific article; zbMATH DE number 2064106
• scientific article; zbMATH DE number 6723376
• scientific article; zbMATH DE number 5510823
• A simple proof of the Brouwer fixed point theorem
• scientific article; zbMATH DE number 62688

Cites work

• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 3714908 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 3793435 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A Weaker Precondition for Loops
• A lattice-theoretical fixpoint theorem and its applications
• Proving total correctness of nondeterministic programs in infinitary logic

Cited in

(14)

• A category-theoretic semantics for unbounded indeterminacy
• Refinement concepts formalised in higher order logic
• There is no fully abstract fixpoint semantics for non-deterministic languages with infinite computations
• Properties of data flow frameworks: A unified model
• Continuity in semantic theories of programming
• A calculus of refinements for program derivations
• Relational semantics revisited
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• A fixpoint theory for non-monotonic parallelism
• The weakest precondition calculus: Recursion and duality
• Repetitions, known or unknown?
• scientific article; zbMATH DE number 3949704 (Why is no real title available?)
• Interpretations of recursion under unbounded nondeterminacy
• scientific article; zbMATH DE number 6723376 (Why is no real title available?)

This page was built for publication: A simple fixpoint argument without the restriction to continuity

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