Table of ContentsPPT Slide This Lecture Z Proverbs Formal Reasoning: What You Should Learn Informal versus Formal Reasoning Formal Proofs using Z Schemas as Hypotheses Schemas as Hypotheses (cont) PPT Slide Schemas as Conclusions Example The Initialization Theorem Example Example (cont) The One-Point Rule Two Useful Identities Example Precondition Calculation Example Preconditions (cont) Example Example (cont) General Reasoning Implementation/Refinement Methods of Refinement in Z Relating Two State Machines PPT Slide Observations Recall PPT Slide Data Refinement in Z Abstraction Function The Initial States Theorem PPT Slide Operation Refinement Relations Schemas General Case Example PPT Slide Applicability (informal) Correctness (informal) |
Author: David Garlan
Email: shawnh@cs.cmu.edu Home Page: http://www.cs.cmu.edu/afs/cs.cmu.edu/academic/class/15671-f97/www/index.html |