Table of Contents
Chapter 12: Immanent Reasoning
PPT Slide
Operations:
Operations:
Schema names as part of a formula
Initial State Proof Obligation:
?d’: P Person ? #d’ <= Max ? #d’ <= Max ? d’ = ?
Constructing Theories about Specifications
(Leave1; Enter1) ? (? Class1 | p? ? d)
Operations:
Operations:
Investigating Preconditions
Operations:
Investigating Preconditions
Investigating Preconditions
Investigating Preconditions
Telephone Book Example:
Telephone Book Example:
dom telephones ? members ?
Totality
PPT Slide
PPT Slide
The schema for DoEnter1 is total because it specifies what happens no matter what values its inputs and before variables have.
Operation Refinement
|
Author: Computer Science Dept.
|