Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Volume 7 / Issue 2

available in:   PDF (336 kB) PS (108 kB)
 
get:  
Similar Docs BibTeX   Write a comment
  
get:  
Links into Future
 
DOI:   10.3217/jucs-007-02-0175

 

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)

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: binary methods, coalgebra, modal logic, specification

Categories: D.2.1, D.2.4, F.3.1, F.4.1