Algebraic-coalgebraic specification in CoCasl
Algebraic-coalgebraic specification in CoCasl
复制标题
CoCasl 中的代数-代数规范
DOI：
10.1016/j.jlap.2005.09.006
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Lutz Schröder
中科院分区：
文献类型：
--
作者：
Till Mossakowski;Horst Reichel;Markus Roggenbach;Lutz Schröder
我们引入CoCasl作为代数规格说明语言CASL的轻量级但富有表现力的余代数扩展。CoCasl允许代数数据类型和协代数进程类型的嵌套组合。此外，它为观察者索引的模态逻辑提供了句法糖分，该逻辑允许例如表达公平性属性。该逻辑包括用于具有结构化等式结果类型的观察者的模运算符的通用定义。我们证明了规范的最终模型的存在，其格式允许使用等式指定的初始数据类型作为观察，以及模式公理。通过进程代数CSP和CCS的规范说明了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.
登录
查看更多内容
HasCasl 中独立于 Monad 的动态逻辑
DOI：
10.1093/logcom/14.4.571
发表时间：
2004
期刊：
J. Log. Comput.
影响因子：
--
作者：
Lutz Schröder;Till Mossakowski
通讯作者：
Till Mossakowski
DOI：
10.1007/978-3-540-44616-3_20
发表时间：
1999
期刊：
Inf. Control.
影响因子：
--
作者：
H. Reichel
通讯作者：
H. Reichel
DOI：
10.1007/978-3-540-40020-2_21
发表时间：
2002
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
Till Mossakowski
通讯作者：
Till Mossakowski
论实数的余代数
影响因子：
5.4
作者：
Dusko Pavlovic;V. Pratt
通讯作者：
V. Pratt
HACASL 中独立于 Monad 的霍尔逻辑
DOI：
10.1007/3-540-36578-8_19
发表时间：
2003
期刊：
J. Univers. Comput. Sci.
影响因子：
--
作者：
Lutz Schröder;Till Mossakowski
通讯作者：
Till Mossakowski