| Table of Contents, relating the papers and the PVS source. | Detailed description of the files in this directory | Download! | Jump to my home page |
All three papers investigate coalgebras for bivariant functors Set x Set --> Set and their properties. Paper [2] is an extended version of [1]. Paper [3] is a successor that deals with some questions that have been left open in [2].
Coalgebras for endofunctors C --> C can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors CxC --> C. This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard results.
A generalised notion of coalgebra that is capable of modelling binary methods as they occur in object-oriented programming has been introduced in [2]. An important problem with this generalisation is that bisimulations are not closed under union and that a greatest bisimulation does not exists in general. There are two possible approaches to improve this situation: First, to strengthen the definition of bisimulation, and second, to place constraints on the coalgebras (i.e., on the behaviour of the binary methods). In this paper I use both approaches to show that (under reasonable assumptions) the greatest bisimulation does exist for all coalgebras of extended polynomial functors.
Althoutgh PVS' dependently typed logic is quite expressive, there are certain limitations. Therefore I could not formalize the class of functors that I discuss in the papers. This implies that also the main propositions of the paper have not been proved within PVS. But for those results that are obtained by induction on the structure of the functor, I formalized the inductive predicate and proved all the induction steps in PVS.
The directory contains also certain prove attempts for lemmas, which do not hold in general. The name of these "non-lemmas" ends in _unprovable, for instance cofib_exp_unprovable in theory FibProps, file fibprops.pvs, which states cofibredness for the exponent of predicates. Of course there are no proofs for unprovable lemmas. I decided to keep these lemmas and their partial proofs in this distribution, because these proof attempts contain valuable information for the construction of counter examples.
All together, this directory contains about 700 Lemmas and more than 9000 proof commands to prove them. This was not only a chellenge for me, it also resulted in more than 40 bug reports for PVS, see here.
M-x load-file pvs-batch.el
You can prove everything by issuing prove-importchain in
theory top, file all.pvs.
| Table of Contents, relating the papers and the PVS source. | Detailed description of the files in this directory | Download! | Jump to my home page |
last changed on 15 Jan 2002 by Hendrik