Chapter 12: Immanent Reasoning

23/10/01


Click here to start


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.