Algebraic-coalgebraic specification in CoCasl

9 years 11 months ago
Algebraic-coalgebraic specification in CoCasl
We introduce CoCasl as a light-weight but expressive coalgebraic extension of the algebraic specification language Casl. CoCasl allows the nested combination of algebraic datatypes and coalgebraic process types. Moreover, it provides syntactic sugar for an observer-indexed modal logic that allows e.g. expressing fairness properties. This logic includes a generic definition of modal operators for observers with structured equational result types. We prove existence of final models for specifications in a format that allows the use of equationally specified initial datatypes as observations, as well as modal axioms. The use of CoCasl is illustrated by specifications of the process algebras CSP and CCS. Key words: Algebraic specification; coalgebra; process algebra; Casl, CCS, CSP. In recent years, coalgebra has emerged as a convenient and suitably general way of specifying the reactive behaviour of systems [52]. Generally, software specifications consist of collections of symbols called...
Till Mossakowski, Lutz Schröder, Markus Rogge
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JLP
Authors Till Mossakowski, Lutz Schröder, Markus Roggenbach, Horst Reichel
Comments (0)