Specification in Fresco

software in the form of abstract classes; and the specification elements of the language can also be used in concrete classes to document the implementations and their development in a style similar to that of [Morgan 90]. It is interesting to contrast Fresco with object-oriented styles of specification: firstly because it is based on VDM [Jones 86], rather than Z; and secondly because of its emphasis on specifying program modules, rather than modularizing specifications. The first difference has little impact on any comparison of style with, say, Object Z; but the second makes a profound difference to our approach to the example. In Fresco, a class can describe a specification or an implementation, or, most commonly, a mixture of the two -- in which case, the programmer ought to verify that the implementation meets the specification. The implementation is described with programming language code, and the specification with class variables (like Object Z's state schema variables),...

• Type: Conference
• Year: 1992
• Where: ZUM
• Authors: Alan Wills
• Keywords: Formal Methods, Object Z, Specification Elements, Specifications, ZUM 1992