Experiment 1: Event-B basic subset to IL0 in *TL

Plan of the first experiment

• Soton to provide basic setup for testing ETL: Soton [14 Dec]
• Start developers’ wiki on eventb.org
• All the bits are to be saved on Soton subversion server
• Define translation rule for:
  • algorithmic: sequential composition, explicit loop, if-then-else: Ncl [20 Dec]
  • mathematical language: arithmetics, functions (N +-> N): Soton [20 Dec]
• Define the overall structure of translation rules, common helper functions and rules: All