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.

Click here to jump downwards to the description.
Source files
queue.beh CCSL source
Queue_model.pvs Model and general results for Queue
ListQueue_model.pvs Model and general results for ListQueue
Queue_refine.pvs Refinement of Queue
Queue_theorem.prf Proofs for theorems in the CCSL specification
proof_save_Queue_basic saved proofs for Queue
Automatic typechek
typecheck.el control file for PVS
all.pvs Import everything
Generated by the CCSL compiler
ccsl_prelude.pvs Semantics of the prelude
Queue_basic.pvs Semantics of Queue
Queue_theorem.pvs The theorems of the Queue specification
ListQueue_basic.pvs Semantics of ListQueue

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