The Coalgebraic Class Specification Language CCSL

Abstract

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 or 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.