A calculus of refinements for program derivations
From MaRDI portal
DOI10.1007/BF00291051zbMATH Open0658.68018OpenAlexW2038814435MaRDI QIDQ1111362FDOQ1111362
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
Recommendations
General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- Program development by stepwise refinement
- Title not available (Why is that?)
- A Powerdomain Construction
- Countable nondeterminism and random assignment
- Title not available (Why is that?)
- Title not available (Why is that?)
- The specification statement
- On correct refinement of programs
- A theoretical basis for stepwise refinement and the programming calculus
- Title not available (Why is that?)
- General correctness: A unification of partial and total correctness
- A Transformation System for Developing Recursive Programs
- Power domains
- Predicative programming Part I
- Proving total correctness of nondeterministic programs in infinitary logic
- Title not available (Why is that?)
- A Weaker Precondition for Loops
- Title not available (Why is that?)
- Title not available (Why is that?)
- A simple fixpoint argument without the restriction to continuity
- Proof of a program
Cited In (59)
- Calculating modules in contextual logic program refinement
- Combining relational calculus and the Dijkstra-Gries method for deriving relational programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Program derivation using the refinement calculator
- Using lattice theory in higher order logic
- Inductive data types for predicate transformers
- A refinement calculus for logic programs
- Freefinement
- Program inversion in the refinement calculus
- Formalization of the semantics of the language Refal
- Exits in the refinement calculus
- Refinement concepts formalised in higher order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Combining angels, demons and miracles in program specifications
- Interfaces for refining recursion and procedures
- Proofs as programs
- Assumption propagation through annotated programs
- Refining exceptions in four-valued logic
- Predicate transformers as power operations
- Title not available (Why is that?)
- Real-time refinement in Manna and Pnueli's temporal logic
- Title not available (Why is that?)
- ERC -- an object-oriented refinement calculus for Eiffel
- Structured derivations: a unified proof style for teaching mathematics
- A core calculus for dynamic delta-oriented programming
- The weakest specifunction
- Using refinement calculus techniques to prove linearizability
- Algebraic foundations for specification refinements
- Mechanizing some advanced refinement concepts
- Superposition refinement of reactive systems
- Title not available (Why is that?)
- Category theoretic models of data refinement
- A theoretical basis for stepwise refinement and the programming calculus
- A specification-oriented semantics for the refinement of real-time systems
- Safe Modification of Pointer Programs in Refinement Calculus
- Title not available (Why is that?)
- Stepwise refinement of heap-manipulating code in Chalice
- Title not available (Why is that?)
- A reification calculus for model-oriented software specification
- Command algebras, recursion and program transformation
- Programming from metaphorisms
- Metaphorisms in programming
- Types and invariants in the refinement calculus
- Title not available (Why is that?)
- Procedure compilation in the refinement calculus
- The lattice of data refinement
- Intuitionistic Refinement Calculus
- A refinement methodology for object-oriented programs
- Linking theories in probabilistic programming
- Verification, refinement and scheduling of real-time programs
- High-Level Programs and Program Conditions
- Modular verification for shared-variable concurrent programs
- Algebraic proofs of consistency and completeness
- Predicate transformers and higher-order programs
- Games and winning strategies
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
Uses Software
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)
