Next:
Introduction
Up:
No Title
Previous:
Petrochemical Tank - Version
Canonical Terms and Proof Obligations
Introduction
Proof Obligation : Canonical Terms (Forms)
Canonical Terms and Reduced Expressions
Proof Obligations : Consistency and Completeness
Consistency
Completeness
Sufficient Completeness
Extensibility (Conservative Extension)
Validating an Algebraic Specification
Termination
Specification of a Set
Requirement
Additional Axioms
Use of Hidden Operations
Specification of a Bag
Other Atomic Constructors for Set
Structural Induction
Canonical Forms for the Stack
Proof of Canonical Property for Stack
Proof of the Sufficient Completeness of Stack
Proof of Canonical Property for Set
Attributes of an Operation
Derivation of Attributes from Axioms
Summary
Lee McCluskey
2002-12-18