Executable Specifications with Quantifiers in the FASE System

Abstract

We present an overview of the FASE system for executable specifications based upon final, rather than initial, algebras. Particular emphasis is placed upon the execution of expressions involving quantifiers. The need for such expressions is explained, as is our method for evaluating them. By permitting quantifiers, we are able to give very natural specifications for many data types. As an example, we give the FASE specification of Kemmerer's library system.