Coalgebraic Methods for Object-Oriented Specification

This page is on my PhD on Coalgebraic Methods for Object-Oriented Specification. The main purpose of this page is to give access to the source code (containing proofs and examples) that has been developed for the thesis. Of course you can also download the PhD itself.

General Information

The PhD is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level. There are two main contributions:

a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be represented
a description of the Coalgebraic Class Specification Language CCSL

This page makes relevant source files available, which are not included in the printed version of the PhD. These source files fulfil the following purposes:

formalise and prove results of the PhD in the theorem prover PVS
illustrate results of the thesis
provide the complete source code for some examples discussed in the PhD

About the contents

The source code is split into four directories:

Fibration: Formalisation of the Fibrations Pred and Rel, proofs and examples of Sections 2.4, 2.6, and Chapter 3. (There is considerable overlap with the material distributed for my binary methods papers.)
Variance: Formalisation of the variance algebra of Section 4.2
Queue: CCSL specification of queues (the running example of Chapter 4), plus the refinement proofs of Subsection 4.10.1
UML: CCSL and PVS source code of the UML example of Subsection 4.10.3

Technicalities

The sources were developed with PVS 2.4 patch level 1. Every directory contains a file typecheck.el. This contains emacs lisp code that, when evaluated in PVS, typechecks all sources of that directory. So to typecheck start PVS in one directory and type

M-x load-file typecheck.el

To prove everything load the file all.pvs and issue prove-importchain.

Home Science Overview All Publications Talks PhD CCSL Robin

last modified on 20 Sep 2011 by Hendrik