Prespecification in data refinement
From MaRDI portal
DOI10.1016/0020-0190(87)90224-9zbMATH Open0624.68027OpenAlexW2152198540MaRDI QIDQ578901FDOQ578901
Authors: Tony Hoare, Jifeng He, Jeff W. Sanders 
Publication date: 1987
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0020-0190(87)90224-9
Recommendations
data refinementabstract data typeconcrete data typenondeterministic procedural programming languagepostspecificationprespecificationweakest specification
Cites Work
- Title not available (Why is that?)
- A calculus of communicating systems
- Proof of correctness of data representations
- Programming as a Discipline of Mathematical Nature
- The weakest prespecification
- Title not available (Why is that?)
- Non-deterministic data types: Models and implementations
- Title not available (Why is that?)
Cited In (30)
- Data refinement by calculation
- Refinement and state machine abstraction
- A pragmatic approach to stateful partial order reduction
- Incompleteness of relational simulations in the blocking paradigm
- Relational concurrent refinement: automata
- Title not available (Why is that?)
- Mechanizing some advanced refinement concepts
- An analysis of refinement in an abortive paradigm
- Abstraction for concurrent objects
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- Data refinement of predicate transformers
- Title not available (Why is that?)
- Normal form approach to compiler design
- The projection of systolic programs
- Correct Hardware Design and Verification Methods
- Relational separation logic
- More relational concurrent refinement: traces and partial relations
- Peirce algebras
- A reification calculus for model-oriented software specification
- Composition and refinement of specifications of parameterized data types
- Relational decomposition
- The lattice of data refinement
- Parallel composition and decomposition of specifications
- Data refinement with probability in mind
- Information flow in systems with schedulers. II: Refinement
- Assume-guarantee reasoning for additive hybrid behaviour
- Temporal-logic property preservation under Z refinement
- Jifeng He at Oxford and beyond: an appreciation
- A single complete rule for data refinement
- A single complete refinement rule for Z
This page was built for publication: Prespecification in data refinement
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q578901)
