Refinement calculus. A systematic introduction
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) General topics in the theory of software (68N01) Semantics in the theory of computing (68Q55)
This book is the first systematic introduction to the mathematical and logical basis of refinement calculus, a framework for reasoning about correctness and refinement of programs. Invented by the first author, this method extends Dijkstra's use of weakest precondition for correctness of programs, where program statements are modeled as predicate transformers. The second author gave it a lattice-theoretic basis, which is used in this book in conjunction with higher-order logic to give a new foundation to refinement calculus. The book is divided in four parts. The first one introduces the foundations of refinement calculus, together with basic notions of lattice-theory and higher-order logic. In the second part the authors describe predicate transformers, then characterize a family of program statements which can be interpreted as predicate transformers having a monotonicity property with respect to the lattice-theoretic interpretation. This part is also the place for describing two other semantics, game semantics and choice semantics: the latter is equivalent to predicate transformers semantics and both are abstractions of the game semantics. The third part deals with recursion and iteration. The classical fixed point theorems of Tarski and Scott are taken advantage of to recursive procedures, loops, and various examples of the use of refinement calculus for sorting algorithms, for solving the N-Queen problem, or two-person games are studied in great detail. Finally, some subclasses of predicate transformers and of statements are studied, especially the important class of conjunctive statements. The authors study the application of refinement calculus to specification statements, the way to do refinement taking the context into account, and the correctness-preserving transformation of iterative structures. The book is thoroughly detailed and illustrated with a lot of examples. Each chapter ends with a historical notice and a series of exercises.
- Refinement and verification in component-based model-driven design
- On the design of correct and optimal dynamical systems and games
- A calculus of refinements for program derivations
- Structured calculational proof
- Fusion and simultaneous execution in the refinement calculus
- A formal model of real-time program compilation
- Soundness of data refinement for a higher-order imperative language
- Annotation inference for modular checkers
- Calculating sharp adaptation rules.
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- A verified ODE solver and the Lorenz attractor
- Designing a semantic model for a wide-spectrum language with concurrency
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Refinement to imperative HOL
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Angelic processes for CSP via the UTP
- Hybrid action systems
- Contracts, games, and refinement.
- Evolution of rule-based programs
- Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism
- On hierarchically developing reactive systems
- An axiomatic approach to existence and liveness for differential equations
- Unifying theories of reactive design contracts
- Abstractions of non-interference security: probabilistic versus possibilistic
- A wide-spectrum language for verification of programs on weak memory models
- Automated verification of reactive and concurrent programs by calculation
- Integrating formal specifications into applications: the ProB Java API
- Traits: correctness-by-construction for free
- Bridging arrays and ADTs in recursive proofs
- Refinement algebra for probabilistic programs
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Kleisli, Parikh and Peleg compositions and liftings for multirelations
- Towards patterns for heaps and imperative lambdas
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Automatic refinement to efficient data structures: a comparison of two approaches
- Consistency-preserving refactoring of refinement structures in Event-B models
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Program algebra for quantitative information flow
- The weakest specifunction
- Programming interfaces and basic topology
- A theory for execution-time derivation in real-time programs
- Assumption propagation through annotated programs
- Modelling and analysing neural networks using a hybrid process algebra
- The refinement calculus of reactive systems
- Continuous functions on final coalgebras
- Angelicism in the theory of reactive processes
- Formalizing the Edmonds-Karp algorithm
- Don't care non-determinism in logic program refinement
- Generic models of the laws of programming
- Automating Induction with an SMT Solver
- The laws of programming unify process calculi
- Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
- Towards an algebra for real-time programs
- Laws of programming for references
- Exploring an interface model for CKA
- A relation-algebraic approach to multirelations and predicate transformers
- A program construction and verification tool for separation logic
- Unifying theories of programming in Isabelle
- Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
- Developments in concurrent Kleene algebra
- Data refinement of invariant based programs
- Patterns for refinement automation
- A refinement methodology for object-oriented programs
- Full abstraction at package boundaries of object-oriented languages
- Algebra of monotonic Boolean transformers
- Generalised rely-guarantee concurrency: an algebraic foundation
- Knowledge and Games in Modal Semirings
- Safe Modification of Pointer Programs in Refinement Calculus
- On the Purpose of Event-B Proof Obligations
- A Practical Single Refinement Method for B
- Multiple Viewpoint Contract-Based Specification and Design
- Intuitionistic Refinement Calculus
- Edmonds-Karp
- Refinement Monadic
- Flow Networks
- Gabow SCC
- Multirelations with infinite computations
- scientific article; zbMATH DE number 517333 (Why is no real title available?)
- Invariant diagrams with data refinement
- Compositional noninterference from first principles
- Connectors as designs: modeling, refinement and test case generation
- Algebraic_VCs
- scientific article; zbMATH DE number 1512629 (Why is no real title available?)
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- scientific article; zbMATH DE number 194642 (Why is no real title available?)
- Reasoning about orchestrations of web services using partial correctness
- Data Refinement
- Computer-aided development of a real-time program
- Unifying Semantics for Concurrent Programming
- The algebra of multirelations
- A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models
- Building Specifications in the Event-B Institution
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- An algebraic approach to multirelations and their properties
- Verified Compilation and the B Method: A Proposal and a First Appraisal
- Concurrent dynamic algebra
- Taming multirelations
- Algebra for quantitative information flow
This page was built for publication: Refinement calculus. A systematic introduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4396958)
