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 Queue

Detailed Desciption for directory UML

This page gives detailed information for all files in the directory UML. All PVS material is in the subdirectory UML/Pvs. Only the CCSL sources are directly in UML.

Click here to jump downwards to the description.
CCSL Sources
setof.beh Ground signature extension
company.beh structured company specification
flat_company.beh flat company specification
Generated Files
Pvs/AnonymousSignature_1__basic.pvs Anonymous ground signature for Rel
Pvs/BaseTypes_basic.pvs for the ground signature BaseTypes
Pvs/Configuration_basic.pvs for the class specification Configuration
Pvs/Department_basic.pvs for the class specification Department
Pvs/Employee_basic.pvs for the class specification Employee
Pvs/FDepartment_basic.pvs for the class specification FDepartment
Pvs/FEmployee_basic.pvs for the class specification FEmployee
Pvs/FProject_basic.pvs for the class specification FProject
Pvs/FlatCompany_basic.pvs for the class specification FlatCompany
Pvs/MapFlatSig_basic.pvs for the ground signature MapFlatSig
Pvs/Project_basic.pvs for the class specification Project
Pvs/RelSig_basic.pvs for the ground signature RelSig
Pvs/SetSig_basic.pvs for the ground signature SetSig
Pvs/ccsl_prelude.pvs for the CCSL prelude
Models for Class specifications
Configuration_model.pvs Model for Configuration
Department_model.pvs Model for Department
Employee_model.pvs Model for Employee
FDepartment_model.pvs final Model for FDepartment
FEmployee_model.pvs final Model for FEmployee
FProject_model.pvs final Model for FProject
FlatCompany_model.pvs Model for FlatCompany
Project_model.pvs final Model for Project
Additional PVS material
MapFlatSig_theory.pvs Properties of mapflatten
RelSig_theory.pvs results for domain/codomain
defs.pvs Utility lemmas
more-assert.pvs additional general material
Equivalence of Structured and Flat company
configuration_compare.pvs equivalence of Configuration and FlatCompany, Part I
configuration_compare_from.pvs equivalence of Configuration and FlatCompany, Part II
department-compare.pvs Equivalence of Department and FDepartment
employee-compare.pvs Equivalence of Project - FProject and of Employee - FEmployee
Saved Proofs
proof_save_Department_basic for Department_basic.pvs
proof_save_Employee_basic for Employee_basic.pvs
proof_save_FDepartment_basic for FDepartment_basic.pvs
proof_save_FEmployee_basic for FEmployee_basic.pvs
proof_save_FProject_basic for FProject_basic.pvs
proof_save_FlatCompany_basic for FlatCompany_basic.pvs
proof_save_Project_basic for Project_basic.pvs
Automatic typechek
typecheck.el control file for PVS
all.pvs Import everything

CCSL Source Files

setof.beh:

This file contains several ground signature extensions in order to work with sets that are needed in both CCSL translations of the company example.

company.beh:

This file contains the structured company specification.

flat_company.beh:

This file contains the flat company specification.

Models for Class Specifications

Configuration_model.pvs, Department_model.pvs, Employee_model.pvs, FDepartment_model.pvs, FEmployee_model.pvs, FProject_model.pvs, FlatCompany_model.pvs, Project_model.pvs: Models

Each of these files contains a model for the corresponding specification, thus proving their consistency.

Additional PVS material

MapFlatSig_theory.pvs:

This file proofs a few properties of mapflatten.

RelSig_theory.pvs:

This file proves that the domain (respectively the codomain) of a finite relation is a finite set.

defs.pvs: General defintions and lemmas

This file maps the comparison operators from CCSL to PVS. It further contains several quite general results about finite sets and cardinalities that are not in the finite sets library of PVS.

more-assert.pvs:

This file serves two purposes. First, it defines predicates that formalise the additional assumptions for the equivalence proof of the structured and flat company specifications. Second, it contains a few general results that are needed in the equivalence proof (for instance that two states of the final FEmployee model are equal if they have identical name and salary).

Equivalence of Structured and Flat company

configuration_compare.pvs, configuration_compare_from.pvs, department-compare.pvs, employee-compare.pvs : Eqivalence proofs

The structured and the flat company specification are equivalent under a few additional assumptions, see Section 4.10.3. These files contain the equivalence proof. The proof is devided in four levels: the equivalences of Project - FProject, Employee - FEmployee, Department - FDepartment, and Configuration - FlatCompany. Each level relies on the previous levels. The precise notion of equivalence that is proved is adhoc. Every level consists of two assertional refinements, such that the graph of each translation map is a bisimulation.

Saved Proofs

proof_save_Department_basic, proof_save_Employee_basic, proof_save_FDepartment_basic, proof_save_FEmployee_basic, proof_save_FProject_basic, proof_save_FlatCompany_basic, proof_save_Project_basic: Saved proofs

The CCSL compiler generates only very few proofs. These files contains all the necessary proofs for the corresponding specifications.

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