ASTD.v, state.v and ASTDstep.v files contain the ASTD semantics definition:
- ASTD.v defines the definition of ASTD language
- state.v defines how the current state of an ASTD is represented
- ASTDstep.v contains the translation of the operationnal semantics of ASTD.
For now, the ASTD language is limited to hierarchical automatas.
B_langage.v, B_state.v and B_semantics.v contain the B language definition:
- B_langage.v contains the definition of the B langage
- B_state.v contains the definition of the structure that represent the current state of a B machine
- B_semantics contains the operationnal semantics of the subset of the B language used in this translation
translation.v file contains the implementation of the translation rules.
stateEquivalence.v file contains the simulation relation between the states of the B machine and the state of the ASTD.
Guard.v file contains the definition of the guards (which are just strings that can be evaluated).
wellConstructed.v defines a predicate that tells if an ASTD is well constructed. It also contains some theorems that are verified for well contructed ASTD.
translationCorrection.v file contains the main theorem (the theorem that says that the ASTD specification simulates the B specification resulting from the translation) and its proof.
The rest of the files contains the proof of the translation. This files are devided into two set of files:
- *Works.v: Each file of this set of files contains the proof that the function stating before "Works" works. For example, translateStateListWorks.v contains the proof that the function translateStateList of translation.v file works.
- theoremsOn*.v: Each file of this set of files contains general theorems on the thing designated ofter "theoremsOn" and their proofs. For example, theoremsOnSubstitutions.v contains general theorems on B substitution.