Data Refinement
This monograph consists of two parts: (1) ten chapters are devoted to the general theory for comparing model oriented data refinement methods and (2) four chapters cover applications including Reynolds' method, the Vienna development method, \(Z\), Hehner's method, Back's refinement calculus and refinement methods due to Abadi and Lynch. In addition, there are four appendices, one of which contains a much needed synopsis of notations introduced in each chapter. Exercise sets are included at the ends of chapters. Some of the exercises require the proof of lemmas or corollaries encountered in a chapter, others involve extensions of ideas presented in a chapter. No solutions to the exercises are given. An extensive bibliography is provided for those interested in pursuing further the material presented in the book. The format for proofs is notable. Each statement in a proof is accompanied by a justification to clarify the statement and the entire proof frequently has line by line discussions of the reason(s) for the proof statement. This format is ideal for those unfamiliar with the approach to data refinement methods. An interesting and worthwhile inclusion is a ``picture gallery of important contributors to the field. Chapter titles follow: Introduction to Data Refinement; Simulation as a Proof Method for Data refinement; Relations and Recursion; Properties of Simulation; Notation and Semantics; A Hoare Logic; Simulation and Hoare Logic; An Extension to Total Correctness; Simulation and Total Correctness; Refinement Calculus; Reynolds' Method; VDM; Z, Hehner's Method, and Back's Refinement Calculus; Refinement Methods due to Abadi and Lamport and to Lynch. This book gathers in one place the state of data refinement methods at the time of its publication.
- Relational concurrent refinement. II: Internal operations and outputs
- Trace-based derivation of a scalable lock-free stack algorithm
- Against digital ontology
- Automated verification of refinement laws
- Hybrid I/O automata.
- Soundness of data refinement for a higher-order imperative language
- State-level and value-level simulations in data refinement
- A hierarchy of failures-based models: theory and application
- Evolution of rule-based programs
- Temporal-logic property preservation under Z refinement
- Bridging arrays and ADTs in recursive proofs
- Model transformations across views
- Composition mechanisms for retrenchment
- On assertion-based encapsulation for object invariants and simulations
- Layout randomization and nondeterminism
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- Generic tools via general refinement
- A sound and complete proof technique for linearizability of concurrent data structures
- Relational concurrent refinement: automata
- Data refinement with probability in mind
- Guarded operations, refinement and simulation
- Verified synthesis of knowledge-based programs in finite synchronous environments
- Levels of abstraction and the Turing test
- Property transformation under specification change
- On the Purpose of Event-B Proof Obligations
- Secure Microkernels, State Monads and Scalable Refinement
- Modelling Divergence in Relational Concurrent Refinement
- Philosophical Conceptions of Information
- scientific article; zbMATH DE number 3943003 (Why is no real title available?)
- Information flow in systems with schedulers. II: Refinement
- Edmonds-Karp
- Refinement Monadic
- Flow Networks
- KBPs
- Gabow SCC
- Worker/Wrapper Transformation
- Model evolution and refinement
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- The mechanical generation of fault trees for reactive systems via retrenchment. I. Combinational circuits
- Verifying a network invariant for all configurations of the Futurebus+ cache coherence protocol
- Category theoretic models of data refinement
- Cogent: uniqueness types and certifying compilation
- Modularising verification of durable opacity
- A Bibliography of Willem-Paul de Roever
- Integrated and automated abstract interpretation, verification and testing of C/C++ modules
- Allegories and collagories for transformation of graph structures considered as coalgebras
- Prpu_Maxflow
- Completeness of ASM refinement
- More relational concurrent refinement: traces and partial relations
- Completeness of fair ASM refinement
- Layout Randomization and Nondeterminism
- Refactoring Object-Oriented Specifications with Data and Processes
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Programming Languages and Systems
- Collagories: relation-algebraic reasoning for gluing constructions
- ASM refinement and generalizations of forward simulation in data refinement: a comparison
- Retrenchment and refinement interworking: the tower theorems
- Blaming the client: on data refinement in the presence of pointers
- Incompleteness of relational simulations in the blocking paradigm
- A probability perspective
- Simple feature engineering via neat default retrenchments
- Alignment complete relational Hoare logics for some and all
- Probabilistic predicate transformers. II: Partially observable probability
- ConcurrentHOL
- File Refinement
- Concerned with the unprivileged: user programs in kernel refinement
- Introducing extra operations in refinement
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
- Relational concurrent refinement. III: Traces, partial relations and automata
- Components as coalgebras: the refinement dimension
- Verifying data refinements using a model checker
- An analysis of refinement in an abortive paradigm
- The specification logic \(\nu \)Z
- Generalising the array split obfuscation
- On using data abstractions for model checking refinements
- Observational purity and encapsulation
- Some proofs of data refinement
- Data refinement and singleton failures refinement are not equivalent
- Stronger compositions for retrenchments
This page was built for publication: Data Refinement
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4702189)
