Theories

This is a collection of machine-checkable theories on various topics. Some of the material that used to be here has been incorporated into the PVS prelude. The set theory related material is now distributed by NASA Langley in the orders and sets_aux theories.

Sequences

The PVS prelude specifies finite sequences and infinite sequences. What do you do if you need a sequence that might be finite or infinite? Various people have formulated answers to that question. For example, see the following:

Here you can find the first (known to me) formalization of finite and infinite sequences using the new PVS support for coalgebraic datatypes. I have tried to follow the NASA team's suggestions for good naming practices. If you have suggestions on how the names might be improved, better approaches to specifying any of the operators, or more results that should be included, please let me know.

sequence.dmp.bz2: note that these theories were developed with the PVS 3.3 release candidate. They will work with PVS 3.2, but due to PVS bug 926 some of the results are marked as proved, but incomplete. Even with the 3.3 release candidate, a few results are marked as proved but incomplete due to PVS bug 948.

sequence-4.0.dmp.gz2: the same theories but proved with PVS 4.0. Note that you need to put the fix for PVS bug 978 (same as bug 948) into your .pvs.lisp file to avoid having some results marked proved but incomplete.

Lamport/Anger Interprocess Communication Axioms

Lamport's interprocess communication axioms, as described in On Interprocess Communication—Part I: Basic Formalism, and Anger's additions to those axioms, as described in On Lamport's Interprocessor Communication Model, are formalized and proved in this PVS collection. One minor error in Lamport's paper was identified and fixed while constructing the PVS formalization. The PVS theories should work with PVS 3.2 and the PVS 3.3 release candidate.

Last modified: Fri May 11 15:13:53 MDT 2007 by Jerry James