The Coalgebraic Class Specification Language CCSL
This paper presents the Coalgebraic Class Specification Language CCSL that is developed within the loop project on formal methods for object-oriented languages(2). CCSL allows the (coalgebraic) specification of behavioral types and classes of object-oriented languages. It uses higher-order logic with universal modal operators to restrict the behavior of objects. A front-end to the theorem provers PVS [ORR + 96] and ISABELLE [Pau94] compiles CCSL specifications into the logic of these theorem provers and allows to mechanically reason about the specifications.
coalgebra specification binary methods modal logic