P may be encoded in the form of a set, but in the framework of B, for example, only certain finite sets are allowed;
Z is more flexible, but no straightforward mechanism is provided for deriving a program from the specification;
the axiom for search, in the algebraic specification of Chapter 10 is actually a schema of axioms; we then have to write down an instance of this schema for every property of interest.
KeywordsFormal Method Type Theory Proof Obligation Proof Assistant Inductive Type
Unable to display preview. Download preview PDF.