This folder contains the final files related to my internship at MIT :

* the Alloy models (ALS)

- a.als : Abstract world, definitions, operations and model consistency.
- b.als : Between world, definition.
- bcif.als : Between and Concrete worlds : initialization and
  finalization.
- bop.als : Between world operations
- bopc.als : Consistency of the Between operations
- c.als : Concrete purse, definition and individual purse operations
- canon.als : Canonicalization constraints
- common.als : Resources common to the Abstract and Concrete worlds (e.g. Coin)
- cop.als : Concrete world operations and model consistency.
- cw.als : Concrete world, definition
- rab.als : Abstract/Between refinement
- rbc.als : Between/Concrete refinement