The Coalgebraic Class Specification Language CCSL

Hendrik Tews

Institut für Theoretische Informatik, TU Dresden

                   tews@tcs.inf.tu-dresden.de

Contents

I. Coalgebras — short intro II. CCSL at work: A coalgebraic Queue specification III. Modal logic IV. Induction & Coinduction nested V. Object-oriented Concepts VI. Binary Methods VII. Conclusion

I. Short Intro  Coalgebras

Coalgebra is a function X ⋯ X ⋯

for instance Aut_{A,B} ⟨out, next⟩ A ⇒ (Aut_{A,B} × B)

Morphisms of Coalgebras as you would expect:  ^{X}_{f}  ^{c} ^{F (X)}_{F (f)}_{Y} _{d} _{F (Y)}

Important concepts

• Bisimulation x R y ⟺ x and y show the same behaviour defined via morphisms [AM89] or via relation lifting [HJ98]

• Invariant if x ∈ P then all successors of x are also in P

• final coalgebra most abstract and contains all possible behaviours

I. Short Intro  Coalgebras & Classes

Coalgebras can model Classes of object-oriented languages

class Point

methods get_x : Self ⟶ real get_y : Self ⟶ real move : Self × real × real ⟶ Self

end Point

Coalgebra c : X T_{P} (X) with
T (X) = ℝ × ℝ × (ℝ × ℝ ⇒ X)

algebraic data types

+

coalgebraic class specifications

+

higher-order logic

= CCSL

I. Short Intro  CCSL Compiler

user lemmas

coalgebraic specification CCSL Compiler

semantics in HOL

Isabelle/HOL or PVS

q.e.d.

models

CCSL  slide 4

II. CCSL at work  Queue Example

Begin Queue[ A : Type ] : ClassSpec

Method put : [Self, A] −> Self; top : Self −> Lift[[A,Self]];

Constructor

new : Self; Assertion Selfvar x : Self

q empty :

x.top ∼ bot Implies Forall(a : A) . x.put(a).top ∼ up(a,x); q filled :

Forall(a1:A, y : Self) . x.top ∼ up(a1,y) Implies

Forall(a2 : A) . x.put(a2).top ∼ up(a1, y.put(a2)); Creation

q new : new.top ∼ bot; Theorem Importing QueueModal[Self,A]

strong reachable : Forall(p, q : Self) :

Let finite? : [Self −> bool] = Lambda(q : Self) :

(Eventually Lambda(x : Self) : x.top = bot For {top}) q IN finite? p And finite? q Implies

(Eventually (Eventually Lambda(r : Self) : r ∼ q For {put}) For {top} ) p;

End Queue

II. CCSL at work  CCSL Overview

• parametrised class specifications – inheritance (of specifications)

– methods, constructor declarations – binary methods

– attributes & update operations – final or loose semantics – axioms for methods and constructors – behavioural equality

– method-wise infinitary modal operators – theorems

• parametrised abstract data types – initial semantics

– no axioms • ground signature extentions

– parametric Types & Terms

– definitions & declarations

• ADT’s and Classes can be nested ⟹ nested induction and coinduction

• higher-order logic

• support for PVS and Isabelle/HOL

• coalgebraic refinement [JT01]

• Version 2.2 available at http://wwwtcs.inf.tu-dresden.de/∼tews/ccsl

III. Modal logic  Greatest Invariants

Invariant is a predicate closed under the coalgebra

in the Queue example: q ∈ P ⟹ ∀a . put(q, a) ∈ P

Invariants form a complete lattice

\underline{P} denotes the greatest invariant contained in P \underline{P} = ⋁ \{Q | Q ⊆ P ∧ Q is an invariant\}

Observe x ∈ \underline{P} then P holds on all direct and indirect successor states of x

III. Modal logic  Always & Eventually

□ (always) acts on predicates (like a variable binder)

□ : (Self Prop) (Self Prop)

in the logic: Γ, x : Self ⊢ φ gives Γ, y : Self ⊢ (□λx : Self . φ) (y).

Semantics

⟦□_{x} φ (y)⟧ = \{(a⃗, b) ∈ ⟦Γ⟧ × ⟦Self⟧ | b ∈ \underline{\{x ∈ ⟦Self⟧ | ⟦φ⟧(a⃗, x)\}} \}

Eventually ♢φ =^{def} ¬□¬φ ( =^{def} λx : Self . ¬(□λy : Self . ¬φ(y)) (x))

Method-wise modal operators arise from subcoalgebras

IV. Induction & Coinduction  Infinite trees with finite width

Begin list[ X : Type ] : Adt

Constructor null : Carrier; cons( car, cdr ) : [X, Carrier] −> Carrier

End list

Begin InfTreeFin[A : Type] : Final ClassSpec

Method

next : Self −> list[[A,Self]]; End InfTreeFin

possibly infinte  • a_{0}  a_{1}  a_{n} • a_{1}^{1}  a_{2}^{1} a_{2}^{1}  •  ⋯  • a_{1}^{n}  a_{2}^{n} a_{2}^{n} •  •  •  ⋯  •  •  • finite

IV. Induction & Coinduction  Nested Proofs

Induction on lists

Coinduction on InfTreeFin

definition Exposing a list algebra on a set X uniquely defines list X Exposing an InfTreeFin coalgebra structure on X uniquely defines X InfTreeFin

proof Any inductive predicate holds on all lists Any InfTreeFin bisimulation is contained in the diagonal (i.e., x R y ⟹ x = y)

Define empty_tree via next(⊥) = null

Define concat via next(p, q) = \{ \begin{matrix}map(λa, p′ . (a, (p′, q))) (next p) & if next p ≠ null \\ map(λa, q′ . (a, (p, q′))) (next q) & if next p = null \end{matrix}

Prove  concat(empty_tree, p) = p  (do induction inside a coinduction)

Validity investigated in [Hen99] V. Object orientation

In general

• “object orientation” applies to software construction systems

• it does not apply to specification languages

• CCSL is a specification language for object-oriented programs

• CCSL gives general support — it does not specialise to the peculiar semantics of a special OO language

CCSL supports

• multiple inheritance

• overriding of methods

• late binding possible

• object identity possible

• dynamic type checking (down casts) possible

Terminology

class specification

class is a model ⟨X, c : X T (X)⟩ (state of an) object is an element x ∈ X

V. Object orientation  Inheritance

Inheritance of specifications • inherits methods & method axioms

• renaming possible

• simple semantics: Let B inherit from A, then

T_{B}(X)  =  T_{A}(X) ×  new methods of B
Signature model of B:  ⟨Y, d : Y  T_{B}(Y)⟩
Semantics of the method axioms wrt. d:  ⟦M_{B}⟧_{d} : Y  Prop
⟦M_{B}⟧_{d}  =  ⟦M_{A}⟧_{π_{1}∘d} ∧  new axioms of B

• π_{1} is like an upcast — but is does not convert the type

• For final semantics: !_{π_{1}∘d} is an static upcast that converts the type of the objects

• Inheritance on specifications does not require inheritance of models

V. Object orientation  Late Binding

Program

class parent = object

method m = 0 end class heir = object inherit parent method m = 1

end

Simple approach

Begin SParent : ClassSpec

Method

m : Self −> nat; Assertion Selfvar x : Self

p1 : x.m <= 1; End SParent Begin SHeir : Classspec Inherit From SParent Assertion Selfvar x : Self

h1 : x.m = 1; End SHeir

V. Object orientation  … Late Binding

More complex approach

Begin SParent : ClassSpec

Method dynamic type : Self −> nat; m : Self −> nat;

Assertion Selfvar x : Self p1 : x.m <= 1; p2 : dynamic type(x) = 0

Implies x.m = 0;

Constructor

new parent : Self; Creation

p3 : dynamic type(new parent) = 0 End SParent Begin SHeir : ClassSpec Inherit From SParent Assertion Selfvar x : Self h1 : dynamic type(x) = 1 Implies x.m = 1;

Constructor

new heir : Self; Creation

h2 : dynamic type(new heir) = 1 End SHeir

VI. Binary Methods  Binary Methods—Example

\underline{Class} A = \{ \underline{method} equal( x : A ) = x == \underline{this} ; \underline{method} memory( env : ℕ ⟶ A ) = ⋯ env(5).equal(\underline{this}) ⋯; \underline{method} strange( f : A ⟶ A ) = ⋯ ;

}

Assume, that X is the state space of the class

equal  : X  (X  bool)
memory : X  (ℕ  X)  ⋯
strange : X  (X  X)  ⋯

Endofunctors cannot describe such signatures!

VI. Binary Methods  Approach

• use bivariant functors H : Set^{op} × Set Set

• Coalgebras are morphisms X  c  H(X, X)

• Morphism of coalgebras: X  c f  H(X, X) H(X, f)H(X, Y) Y  d  H(Y, Y) H(f, Y)

• restrict to polynomial functors inductively built from constants, identity, +, ×, and ⇒

• see [Tew01, Tew02b, Tew02a]

VI. Binary Methods  Extending polynomial functors

Class of Functors  Property  Example

cartesian  Set  Set

K = A | Id | K_{1} + × K_{2} no arguments

Self ⋯

polynomial  Set  Set

F = A | Id | F_{1} + × F_{2} | A ⇒ F_{1} constant arguments

Self × A ⋯

extended cartesian

Set^{op} × Set  Set

G^{K} = A | Id | G_{1}^{K} + × G_{2}^{K} | K ⇒ G_{1}^{K} no functional arguments

Self × Self × Self  ⋯ Self × (Self + A)  ⋯

extended polynomial

Set^{op} × Set  Set

G^{F} = A | Id | G_{1}^{F} + × G_{2}^{F} | F ⇒ G_{1}^{F} functional arguments with constant domain

Self × (A ⇒ Self) ⋯

higher-order polynomial

Set^{op} × Set  Set

H = A | Id | H_{1} + × H_{2} | H_{1} ⇒ H_{2} arbitrary arguments

Self × (Self ⇒ A)  ⋯ Self × (Self ⇒ Self)  ⋯

VI. Binary Methods  Bisimulation

Consider a higher-order polynomial functor H and two coalgebras c : X ⟶ H(X, X) and d : Y ⟶ H(Y, Y).

Bisimulations according to Hermida & Jacobs [HJ98]

• R is a bisimulation for c and d, if

∀x ∈ X, y ∈ Y . R(x, y) implies Rel(H)(R, R)(c(x), d(y))

Bisimulations according to Aczel & Mendler [AM89]

X c  R π_{1}  π_{2}  Yd H(X, X) H(π_{1}, X)  H(R, R) H(R, π_{1}) H(R, π_{2})  H(Y, Y) H(π_{2}, Y) H(R, X)  H(R, Y)

Both notions coincide for extended polynomial functors (in general they are different)

VI. Binary Methods  Relation lifting

Relation lifting (for a h.-o. pol. functor H) is an operation on relations

(S ⊆ U × V, R ⊆ X × Y )  Rel(H)(S, R) ⊆ H(U, X) × H(V, Y)

Defined by induction on the structure of H:

H  Rel(H)  a ∈ H(U, X) b ∈ H(V, Y)
X  R  R(a, b)
A  =_{A}  a =_{A} b
H_{1} × H_{2}  Rel(H_{1}) ×_{R} Rel(H_{2})  Rel(H_{1})(S, R)(π_{1} a, π_{1} b) ∧ Rel(H_{2})(S, R)(π_{2} a, π_{2} b)

H_{1} + H_{2}  Rel(H_{1}) +_{R} Rel(H_{2})  \{ \begin{matrix}if (a, b) = (κ_{1} a_{1}, κ_{1} b_{1}) & Rel(H_{1})(S, R)(a_{1}, b_{1}) \\ if (a, b) = (κ_{2} a_{2}, κ_{2} b_{2}) & Rel(H_{2})(S, R)(a_{2}, b_{2}) \\ otherwise & ⊥ \end{matrix}

H_{1} ⇒ H_{2}  Rel(H_{1}) ⇒_{R} Rel(H_{2})  ∀(u, v) ∈ Rel(H_{1})(R, S) . Rel(H_{2})(S, R)(a(u), b(v))

VI. Binary Methods  Properties

Extension

polynomial structural properties + greatest bisimulations + final models

extended cartesian structural properties + greatest bisimulations equivalences for all coalgebras

extended polynomial structural properties + greatest bisimulations equivalences for finitely based coalgebras

higher-order  only trivial properties

• Results/Examples have been checked/developed with pvs.

see http://wwwtcs.inf.tu-dresden.de/∼tews/binary/

• can allow list : Set Set

VI. Binary Methods  Structural Properties

Let G : Sets^{op} × Sets Sets be a extended polynomial functor. Proposition 1 Relation lifting for G is fibred, i.e. commutes with substitution. Proposition 2 Bisimulations and invariants are closed under arbitrary nonempty intersections. Proposition 3 Bisimulations are closed under composition. Proposition 4 The image ∐_{f} P of a morphism with respect to an invariant P

is an invariant.

Proposition 5 Invariants correspond to subcoalgebras and vice versa. Proposition 6 The predicate ∐_{π_{1}} R is an invariant for any bisimulation R. Proposition 7 The relation π∗_{1}P ∩ R is a bisimulation for any invariant P

and any bisimulation R.

Proposition 8 The predicate P is an invariant if and only if ∐_{δ} P is a bisimulation. Proposition 9 A function is a G–coalgebra morphism if and only if its graph is a bisimulation. Proposition 10 The kernel of a G–morphism is a bisimulation. Proposition 11 The Aczel/Mendler approach and the Hermida/Jacobs approach

yield identical notions of invariant and bisimulation.

CCSL  slide 21

VI. Binary Methods  Final Models

Proposition 12 If a class signature A contains a binary method m, then the associated signature functor H_{A} has a final coalgebra if and only if H_{A}(1, 1) is a singleton.

Proof

1. Assume H has a final coalgebra, say z : Z H(Z, Z).

2. Construct a new coalgebra z′ : Z + 1 H(Z + 1, Z + 1) such that

• the inclusion ι : Z Z + 1 is a coalgebra morphism and • for all y ∈ Z : m_{z′}(⊥, ι y) ≠ m_{z}(y, y).

3. Note, that if f : Z + 1  Z is a coalgebra morphism z′  z, then f ∘ ι = id_{Z}.

4. Conclude, that there is no such morphism z′ z by construction:

m_{z}(⧆, ⧆) = m_{z}(⧆, (f ∘ ι)⧆) = m_{z′}(⊥, ι ⧆)  □

VI. Binary Methods  Example: Union of Bisimulations

Functor K(Y, X) =^{def} Y ⇒ bool

corresponding to one method equal : Self × Self bool

K–bisimulation R ⊆ X × X c : _{X} _{X ⇒ bool}

∀x, x′, y, y′ : X . x R x′ ∧ y R y′ ⟹ c x y = c x′ y′

Defining a K–coalgebra X =^{def} {x_{1}, x_{2}}

c : X  X ⇒ bool  c x y =^{def} if x = y then⊤ else⊥ endif

• Eq(X) = {(x_{1}, x_{1}), (x_{2}, x_{2})} is a bisimulations for c

• R ⊆ X × X =^{def} {(x_{1}, x_{2}), (x_{2}, x_{1})} is a bisimulation for c

• However, Eq(X) ∪ R = X × X is not a bisimulation ⊤ = c x_{1} x_{1} ≠ c x_{1} x_{2} = ⊥

CCSL  slide 23

VI. Binary Methods  Example: Greatest Bisimulation for EPF

Functor G(Y, X) =^{def} (ℕ ⇒ Y) ⇒ bool

Defining a G–coalgebra on �

c : ℕ  (ℕ ⇒ ℕ) ⇒ bool  c x f = \{ \begin{matrix}⊤ & ∃n . ∀i . f i < n \\ ⊥ & otherwise \end{matrix}

G–bisimulation for c R ⊆ ℕ × ℕ

∀x, y : ℕ, f, g : ℕ ℕ . x R y ∧ (∀n . (f n) R (g n)) ⟹ c x f = c y g

Family (S_{n})_{n∈�} i S_{n} j ⟺ i = j ∨ (i < n ∧ j < n)

• all S_{n} are bisimulations

• every finite subset of S_{n}’s has an upper bound (which is a bisimulation)

• _{⋃n} S_{n} = ℕ × ℕ is not a bisimulation, take f_{0} : ℕ ℕ with f_{0} n = 0 and id_{ℕ} :

∀n . (n, 0) ∈ _{⋃n} S_{n} but

⊤ = c 0 id_{ℕ} ≠ c 0 f_{0} = ⊥

VII. Conclusion  Related Work

[1] M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, New York, 1996.

[2] C. Cîrstea. A coalgebraic equational approach to specifying observational structures. In B. Jacobs and J. Rutten, editors, Coalgebraic Methods in Computer Science ’99, volume 19 of ENTCS. Elsevier, Amsterdam, 1999.

[3] R. Hennicker and A. Kurz. (Ω, Ξ)–Logic: On the algebraic extension of coalgebraic specifications. In B. Jacobs and J. Rutten, editors, Coalgebraic Methods in Computer Science ’99, volume 19 of ENTCS, pages 195–212. Elsevier, 1999.

[4] P. D. Mosses. CoFI: The common framework initiative for algebraic specification and development. In M. Bidoit and M. Dauchet, editors, TAPSOFT ’97: Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 115–140. Springer-Verlag, 1997.

[5] T. Mossakowski. CASL: From semantics to tools. In S. Graf and M. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 93–108. Springer, 2000.

[6] Grigore Roşu. Hidden Logic. PhD thesis, University of California at San Diego, 2000.

[7] P. Kellomäki. Mechanical Verification of Invariant Properties of DisCo Specifications. PhD thesis, Tampere University of Technology, Finland, 1997.

VII. Conclusion

Applications

• MSMIE (multiprocessor shared-memory information exchange) protocol

• memory management in the micro kernel operating system

Future work

• CCSL is not actively developed currently

• Application in the VFiasco project — Verification of Fiasco

[1] H. Tews, H. Härtig, and M. Hohmuth. VFiasco — towards a provably correct μ–kernel. Technical Report TUD-FI01-1 – January 2001, TU Dresden, 2001.

[2] M. Hohmuth, H. Tews, and S. G. Stephens. Applying source-code verification to a microkernel — the VFiasco project (extended abstract). In Proceedings of the Tenth ACM SIGOPS European Workshop, September 2002.

  Visit http://www.vfiasco.org

• CCSL Version 3 (brainstorming)

– general specifications with loose/initial/final semantics; multiple sorts

– partial operations

– generic specifications, signature morphisms

VII. Conclusion  References

[AM89] P. Aczel and P. F. Mendler. A final coalgebra theorem. In D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poigné, editors, Proceedings of the Conference on Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science, pages 357–365, Berlin, September 1989. Springer.

[Hen99] U. Hensel. Definition and Proof Principles for Data and Processes. PhD thesis, Univ. of Dresden, Germany, 1999.

[HJ98] C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. Information and Computation, 145(2):107–152, 1998.

[JT01] B. Jacobs and H. Tews. Assertional and behavioural refinement in coalgebraic specification. Submitted, 2001.

[Tew01] H. Tews. Coalgebras for binary methods: Properties of bisimulations and invariants. Theoretical informatics and applications, 35(1):83–111, February 2001.

[Tew02a] H. Tews. Coalgebraic Methods for Object-Oriented Specification. PhD thesis, University of Dresden, 2002. available via wwwtcs.inf.tu–dresden/∼tews/PhD.

[Tew02b] H. Tews. Greatest bisimulations for binary methods. In L. Moss, editor, Coalgebraic Methods in Computer Science ’02, volume 65.1 of ENTCS. Elsevier, Amsterdam, 2002.

Appendix  Invariants

Consider a higher-order polynomial functor H and a coalgebras c : X ⟶ H(X, X). Invariants according to Hermida & Jacobs

• P is an invariant for c, if

∀x ∈ X . P (x) implies Pred(H)(P, P)(c(x))

Invariants according to Aczel & Mendler

P ⊆ X  ι  Xc H(P, P) H(P, ι)  H(X, X) H(ι, X) H(P, X)

Both notions coincide for extended polynomial functors (in general they are different)

CCSL  slide 28

Appendix  Predicate lifting

Predicate lifting is an operation on predicates

(Q ⊆ Y, P ⊆ X)  Pred(H)(Q, P) ⊆ H(Y, X)

Defined by induction on the structure of H:

H  Pred(H)(Q, P)(a) for a ∈ H(Y, X)
X  P (a)
A  ⊤
H_{1} × H_{2}  Pred(H_{1})(Q, P)(π_{1} a) ∧ Pred(H_{2})(Q, P)(π_{2} a)

H_{1} + H_{2}  \{ \begin{matrix}if a = κ_{1} a_{1} & Pred(H_{1})(Q, P)(a_{1}) \\ if a = κ_{2} a_{2} & Pred(H_{2})(Q, P)(a_{2}) \end{matrix}

H_{1} ⇒ H_{2}  ∀u ∈ Pred(H_{1})(P, Q) . Pred(H_{2})(Q, P)(a(u))