On Certification of Specifications for TROLL \it light\/ Objects

TitleOn Certification of Specifications for TROLL \it light\/ Objects
Publication TypeConference Proceedings
Year of Conference1994
AuthorsConrad, S.
Conference NameProc1 9th Workshop on Abstract Data Types - 4th Compass Workshop (ADT'92)
PublisherSpringer, LNCS 785

In this paper we informally present a certification calculus for the object specification language TROLL \it light. The language supports the state- and behavior-oriented specification of information systems. It allows orthogonal construction of large systems from subsystems. The certification calculus provides a basis for verifying properties of specified objects. Besides an introduction to this calculus we show how formulae of this calculus can be derived from TROLL \it light\/ specifications. The transformation from specification language into calculus shall later be done automatically. Furthermore, we demonstrate proving of object properties by means of an example.