An introduction to coalgebraic specification is presented via examples. A coalgebralc specification describes a collection of coalgebras satisfying certain assertions. It is thus an axiomatic description of a particular class of mathematical structures. Such specifications are especially suitable for state-based dynamical systems in general, and for classes in object-oriented programming languages in particular. This chapter will gradually introduce the notions of bisimilarity, invariance, component classes, temporal logic and refinement in a coalgebraic setting. Besides the running example of the coalgebraic specification of (possibly infinite) binary trees, a specification of Peterson's mutual exclusion algorithm is elaborated in detail.
CITATION STYLE
Jacobs, B. (2002). Exercises in Coalgebraic Specification (pp. 237–281). https://doi.org/10.1007/3-540-47797-7_7
Mendeley helps you to discover research relevant for your work.