JUCS - Journal of Universal Computer Science 7(2): 175-193, doi: 10.3217/jucs-007-02-0175
The Coalgebraic Class Specification Language CCSL
expand article infoJan Rothe‡, Hendrik Tews‡, Bart Jacobs§
‡ Institut Theoretische Informatik, TU Dresden, Dresden, Germany§ Department Computer Science, Univ. Nijmegen, Netherlands

Corresponding author: Jan Rothe ( janr@tcs.inf.tu-dresden.de )

© Jan Rothe, Hendrik Tews, Bart Jacobs.
This article is freely available under the J.UCS Open Content License.
Citation: Rothe J, Tews H, Jacobs B (2001) The Coalgebraic Class Specification Language CCSL. JUCS - Journal of Universal Computer Science 7(2): 175-193. https://doi.org/10.3217/jucs-007-02-0175
Open Access
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 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
coalgebra, specification, binary methods, modal logic