The Coalgebraic Class Specification Language CCSL
Jan Rothe (Institut Theoretische Informatik, TU Dresden, Germany)
Hendrik Tews (Institut Theoretische Informatik, TU Dresden, Germany)
Bart Jacobs (Department Computer Science, Univ. Nijmegen, The Netherlands)
This paper presents the Coalgebraic Class Specification Language CCSL that is developed within the loop project on formal methods for object-oriented languages. 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.
Keywords: binary methods, coalgebra, modal logic, specification
Categories: D.2.1, D.2.4, F.3.1, F.4.1