Quick Index

• _____ .
• This Lecture .
• You Should Know .
• Informal versus Formal Reasoning .
• Formal Proofs using Z .
• Schemas as Hypotheses .
• Schemas as Hypotheses (cont) .
• _____ .
• 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 .
• _____ .
• _____ .
• Observations .
• Recall .
• _____ .
• Data Refinement in Z .
• Abstraction Function .
• The Initial States Theorem .
• _____ .
• Operation Refinement .
• Relations .
• Schemas .
• General Case .
• Example .
• _____ .
• Applicability (informal) .
• Correctness (informal) .

These pages and the information above are (c)1996 copyright CMU Computer Science unless stated otherwise.