A calculus of refinements for program derivations

DOI10.1007/BF00291051zbMath0658.68018OpenAlexW2038814435MaRDI QIDQ1111362

Ralph-Johan Back

Publication date: 1988

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

Full work available at URL: https://doi.org/10.1007/bf00291051

zbMATH Keywords

correctnessprogram transformationsemanticsprogram development

Mathematics Subject Classification ID

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

Related Items

A specification-oriented semantics for the refinement of real-time systems ⋮ Predicate transformers as power operations ⋮ Superposition refinement of reactive systems ⋮ Structured derivations: a unified proof style for teaching mathematics ⋮ Using refinement calculus techniques to prove linearizability ⋮ Modular verification for shared-variable concurrent programs ⋮ Safe Modification of Pointer Programs in Refinement Calculus ⋮ Command algebras, recursion and program transformation ⋮ Refinement concepts formalised in higher order logic ⋮ Linking theories in probabilistic programming ⋮ Predicate transformers and higher-order programs ⋮ Games and winning strategies ⋮ Inductive data types for predicate transformers ⋮ Combining angels, demons and miracles in program specifications ⋮ The weakest specifunction ⋮ Calculating modules in contextual logic program refinement ⋮ Exits in the refinement calculus ⋮ Program inversion in the refinement calculus ⋮ Real-time refinement in Manna and Pnueli's temporal logic ⋮ Category Theoretic Models of Data Refinement ⋮ Verification, refinement and scheduling of real-time programs ⋮ Mechanizing some advanced refinement concepts ⋮ The lattice of data refinement

Uses Software

• Find

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• A simple fixpoint argument without the restriction to continuity
• Proving total correctness of nondeterministic programs in infinitary logic
• On correct refinement of programs
• Power domains
• General correctness: A unification of partial and total correctness
• Predicative programming Part I
• Countable nondeterminism and random assignment
• A Weaker Precondition for Loops
• A Transformation System for Developing Recursive Programs
• A Powerdomain Construction
• The specification statement
• An axiomatic basis for computer programming
• Program development by stepwise refinement
• Proof of a program