Chapter 13 Reification and Decomposition


Click here to start

Table of Contents

Chapter 13 Reification and Decomposition

Z Specifications


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


Applicability of Enter2

Correctness of Enter2

Author: Computer Science Dept.