Adrian Hoe’s Reviews > The Way of Z: Practical Programming with Formal Methods > Status Update

Chapter 15 introduces formal reasoning and laws to proof the Z text we have written is in consistency. Every system has an initial state when it starts up. This chapter also introduces Initialization Theorem.

Chapter 14 is a short chapter that introduces generic definitions and free types. It also briefly describes generic schemas.

Done reading chapter 13: Schema types and binding. This chapter shows how to use schemas to define new data typed and also explains the mathematical meaning or semantics of schemas.

Schema Calculus: revisit schema conjunction and disjunction and everything becomes clearer in chapter 12. Besides, this chapter introduces schema composition and piping as well as the less than useful schema negation.

Had a complete review of discrete mathematics in chapter 11. Z provides many conveniences and abbreviations to make Z definitions more readable and easy to understand. Now moving on to chapter 12 Schemas and schema calculus.

"Lambda expression provides abbreviation for a set comprehension and retains the same declaration, predicate and expression structure." Very useful for defining one-time functions.

Completed chapter 10 where logical connectives such as conjunction, disjunction, negation, equivalence and implication give me a clear picture in both logic and natural language. The universal quantification is more frequently used than existential quantification but they are both versatile and powerful definition with the later more a definition for precondition.

"It is not possible to translate natural language requirements into logical formulas by rote or by some mechanical process. It requires deep understanding,..."

Finally completed chapter 9 which the concepts presented is a little harder to grasp.