On correct refinement of programs

DOI10.1016/0022-0000(81)90005-2MaRDI QIDQ1157144zbMATH OpenOpenAlexFDO

Authors Ralph-Johan Back

Publication date 1981

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0022-0000(81)90005-2

zbMATH Keywords

fixpoint semanticspredicate transformersprogram verificationstepwise refinement technique

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A constructive approach to the problem of program correctness
• A Powerdomain Construction
• A Transformation System for Developing Recursive Programs
• Goal-Directed Program Transformation
• scientific article; zbMATH DE number 3649968 (Why is no real title available?)
• scientific article; zbMATH DE number 3651736 (Why is no real title available?)
• scientific article; zbMATH DE number 3679161 (Why is no real title available?)
• scientific article; zbMATH DE number 3694563 (Why is no real title available?)
• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3733226 (Why is no real title available?)
• scientific article; zbMATH DE number 3562462 (Why is no real title available?)
• scientific article; zbMATH DE number 3621081 (Why is no real title available?)
• scientific article; zbMATH DE number 3630737 (Why is no real title available?)
• scientific article; zbMATH DE number 3635472 (Why is no real title available?)
• scientific article; zbMATH DE number 3368143 (Why is no real title available?)
• Initial Algebra Semantics and Continuous Algebras
• Program development by stepwise refinement
• Program Improvement by Source-to-Source Transformation
• Programming as a Discipline of Mathematical Nature
• Proving programs correct through refinement
• The denotational semantics of programming languages

Cited in

(18)

• A calculus of refinements for program derivations
• Combining angels, demons and miracles in program specifications
• The weakest precondition calculus: Recursion and duality
• Parallel composition and decomposition of specifications
• Predicate transformers as power operations
• Integrating formal specifications into applications: the ProB Java API
• Temporal reasoning through automatic translation of tock-CSP into timed automata
• Relational demonic fuzzy refinement
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• Generalised rely-guarantee concurrency: an algebraic foundation
• Deutsch Schorr Waite
• Refinement and state machine abstraction
• Predicate transformers and higher-order programs
• History-based reasoning about behavioral subtyping (extended paper)
• History-based reasoning about behavioral subtyping
• Formalization of Refinement Calculus for Reactive Systems
• Algebra of Monotonic Boolean Transformers
• Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm

This page was built for publication: On correct refinement of programs

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