Table of Contents,
relating the PhD and the online material
of the files in this directory
Coalgebraic Methods for Object-Oriented Specification
This page is on my PhD on
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.
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:
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
- 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:
- 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
- Formalisation of the variance algebra of Section 4.2
- CCSL specification of queues (the running example of Chapter
4), plus the refinement proofs of Subsection 4.10.1
- CCSL and PVS source code of the UML example of Subsection 4.10.3
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
To prove everything load the file all.pvs
and issue prove-importchain.
M-x load-file typecheck.el
last modified on
20 Sep 2011