Detailed Descriptions: Fibration Variance Queue

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 |

```
``````
M-x load-file typecheck.el
```

Home Science Overview All Publications Talks PhD CCSL Robin

last modified on 20 Sep 2011 by Hendrik