Table of Contents
Chapter 13 Reification and Decomposition
Z Specifications
Operations:
Specification, Design, Implementation
Data Reification
Modelling Sets by Sequences
Retrieve Function
Operation Modelling
Prove Correctness of the Representation
PPT Slide
Case 1: x ?ran r implies append(<x> ^ ?, r) = append (?, r)
Case 2: x ?ran r
Modelling Set Intersection
Modelling Set Difference
Reification & Decomposition with Schemas
Example Design and Specification
Relating Specification and Design
Correctness of Design
Proof:
Applicability of Enter2
Correctness of Enter2
|
Author: Computer Science Dept.
|