A calculus of refinements for program derivations

DOI10.1007/BF00291051MaRDI QIDQ1111362zbMATHOpenAlexFDO

Authors 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

semanticscorrectnessprogram transformationprogram development

Mathematics Subject Classification ID

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

Recommendations

• A theoretical basis for stepwise refinement and the programming calculus
• Refinement Calculus
• Formal models of stepwise refinements of programs
• A refinement calculus for logic programs
• scientific article; zbMATH DE number 512961

Cites work

• scientific article; zbMATH DE number 4047034 (Why is no real title available?)
• scientific article; zbMATH DE number 3679161 (Why is no real title available?)
• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3748394 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 3621081 (Why is no real title available?)
• scientific article; zbMATH DE number 3266609 (Why is no real title available?)
• A Powerdomain Construction
• A Transformation System for Developing Recursive Programs
• A Weaker Precondition for Loops
• A simple fixpoint argument without the restriction to continuity
• A theoretical basis for stepwise refinement and the programming calculus
• An axiomatic basis for computer programming
• Countable nondeterminism and random assignment
• General correctness: A unification of partial and total correctness
• On correct refinement of programs
• Power domains
• Predicative programming Part I
• Program development by stepwise refinement
• Proof of a program
• Proving total correctness of nondeterministic programs in infinitary logic
• The specification statement

Cited in

(59)

• High-Level Programs and Program Conditions
• Real-time refinement in Manna and Pnueli's temporal logic
• The lattice of data refinement
• Mechanizing some advanced refinement concepts
• Using refinement calculus techniques to prove linearizability
• scientific article; zbMATH DE number 1696507 (Why is no real title available?)
• Types and invariants in the refinement calculus
• A specification-oriented semantics for the refinement of real-time systems
• Algebraic foundations for specification refinements
• A refinement calculus for logic programs
• Program inversion in the refinement calculus
• Safe Modification of Pointer Programs in Refinement Calculus
• Combining angels, demons and miracles in program specifications
• scientific article; zbMATH DE number 2013579 (Why is no real title available?)
• scientific article; zbMATH DE number 732050 (Why is no real title available?)
• A reification calculus for model-oriented software specification
• Command algebras, recursion and program transformation
• scientific article; zbMATH DE number 177257 (Why is no real title available?)
• scientific article; zbMATH DE number 1512629 (Why is no real title available?)
• scientific article; zbMATH DE number 1512613 (Why is no real title available?)
• Procedure compilation in the refinement calculus
• Algebraic proofs of consistency and completeness
• Predicate transformers and higher-order programs
• Games and winning strategies
• scientific article; zbMATH DE number 48517 (Why is no real title available?)
• scientific article; zbMATH DE number 512961 (Why is no real title available?)
• scientific article; zbMATH DE number 1670751 (Why is no real title available?)
• Interfaces for refining recursion and procedures
• ERC -- an object-oriented refinement calculus for Eiffel
• A bi-directional refinement algorithm for the calculus of (co)inductive constructions
• scientific article; zbMATH DE number 1617299 (Why is no real title available?)
• Freefinement
• Proofs as programs
• Category theoretic models of data refinement
• Refining exceptions in four-valued logic
• Structured derivations: a unified proof style for teaching mathematics
• Programming from metaphorisms
• A core calculus for dynamic delta-oriented programming
• Predicate transformers as power operations
• A theoretical basis for stepwise refinement and the programming calculus
• Calculating modules in contextual logic program refinement
• Formalization of the semantics of the language Refal
• Stepwise refinement of heap-manipulating code in Chalice
• Exits in the refinement calculus
• Combining relational calculus and the Dijkstra-Gries method for deriving relational programs
• Modular verification for shared-variable concurrent programs
• scientific article; zbMATH DE number 497680 (Why is no real title available?)
• Linking theories in probabilistic programming
• Intuitionistic Refinement Calculus
• The weakest specifunction
• A refinement methodology for object-oriented programs
• Program derivation using the refinement calculator
• Using lattice theory in higher order logic
• Metaphorisms in programming
• Refinement concepts formalised in higher order logic
• Assumption propagation through annotated programs
• Inductive data types for predicate transformers
• Superposition refinement of reactive systems
• Verification, refinement and scheduling of real-time programs

Describes a project that uses

Uses Software

• Find

This page was built for publication: A calculus of refinements for program derivations

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