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

Rothe, Jan; Tews, Hendrik; Jacobs, Bart

J. UCS 7, No. 2, Spec. Iss., 175-193 (2001).

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

Keywords:

coalgebraic class specification language

Software:

OCaml; CCSL; PVS