PhD navigation: Table of Contents, relating the PhD and the online material Detailed description of the files in this directory Download area

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: 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:

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