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

Detailed Descriptions:
Fibration
Variance
UML

# Detailed Desciption for directory `Queue`

This page gives detailed information for all files in the
directory `Queue`.

## General theory

#### queue.beh: CCSL Specification

This file contains two CCSL specifications: `Queue` and
`ListQueue`.

#### Queue_model.pvs: Model and
general results for Queue

This file contains the model of Example 4.4.6. It further
contains a few general notions and results: The notion of
computaion path' for Queues and a charicterisation of the modal
operators. Finally there are the essentials of the proof of
Equation 4.2 and 4.3 in Example 4.5.10.

#### ListQueue_model.pvs: Model
and general results for ListQueue

This file contains a model for the ListQueue Specification and a
characterisation of bisimilarity.

#### Queue_refine.pvs: Refinement

This file contains the refinement proof that is used as an
example in Section 4.10.1. It shows that the specification
ListQueue is an assertional refinement of the specification
Queue.

#### Queue_theorem.prf: Proofs for
theorems

This file contains the proofs for the theorems in the Queue
specification. These proof scripts only invoke lemmas from the file Queue_modal.pvs. When
processing the Queue specification the CCSL compiler generates
the file Queue_theorem.pvs. The
CCSL compiler does not overwrite Queue_theorem.prf.

#### proof_save_Queue_basic:
Saved proofs for Queue

The CCSL compiler generates only very few proofs. This file
contains all proofs for Queue_basic.pvs that are necessary to
proof all lemmas in this directory. To use this file run first
the CCSL compiler and copy then `proof_save_Queue_basic`
over `Queue_basic.prf`.

## Automatic type check

#### all.pvs: Import everything

Use this theory to run all proofs via `prove-importchain`.

#### typecheck.el: typecheck everything

To
typecheck everything start PVS in this directory and type
```
M-x load-file typecheck.el
```

Home
Science Overview
All Publications
Talks
PhD
CCSL
Robin

last modified on
20 Sep 2011
by Hendrik