×

The coalgebraic class specification language CCSL. (English) Zbl 0970.68104

Summary: 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 and ISABELLE compiles CCSL specifications into the logic of these theorem provers and allows to mechanically reason about the specifications.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T27 Logic in artificial intelligence

Software:

OCaml; CCSL; PVS
PDF BibTeX XML Cite