A New Definitional Specification Language

摘要

In this paper we present a new Definitional Specification Language (DSL), which is based on an extended first order predicate calculus. The basic building blocks are pristines and definitions. A pristine is a ground predicate and a definition is a logical expression made of pristines and other definitions. First order predicate calculus is enriched with three key concepts a resource, a transitional and a state type to facilitate the specification of dynamic behaviors. Resultant specification is clear with no cumbersome manipulation of time variables. Domain theorems can be generated where insights, into a specification, are brought to light and analyzing them helps to resolve ambiguities, which may arise. Modularity is automatically accomplished by definitions construction. Hierarchical specification is achieved by use of strong relationships between definitions; in what it might be a top-down or bottom-up approach. To illustrate the basics of DSL, a specification from the world of fruits will be provided where no typing is involved.