Définition d'un langage impératif avec test de positivité

Le but du projet est de définir un autre langage de programmation, légèrement différent de celui utilisé en cours.

1. Le langage des expressions arithmétiques sera nommé eexpr,
2. Le langage des instructions sera nommé exo,
3. Les expressions arithmétiques contiendront également une multiplication et une soustraction,
4. Il n'y aura pas d'expressions booléennes,
5. L'instruction while ne sera pas présente dans le langage (et c'est tant mieux puisqu'il n'y a pas d'expressions booléennes),
6. En revanche on trouvera deux instructions de contrôle, basées sur la positivité d'un argument numérique:
   • while e positive i end loop
   • if e positive i otherwise i'

Il faudra fournir tous les éléments suivants:

1. définir la sémantique naturelle de ce langage sous forme d'un prédicat nommé sn' (dans le même style que la sémantique naturelle donnée comme référence pour les expressions expr et les instructions instr)
2. Un traducteur de aexpr vers eexpr devra être fourni,
3. Un traducteur de instr vers exo devra être fourni,
4. Une preuve que le traducteur est correct, au moyen d'un énoncé qui aura la forme suivante:

   forall (p:exo)(r r':env), exec r (translate p) r' <-> sn' r p r'
   

5. Un analyseur syntaxique pour le nouveau langage

Je conseille d'organiser ce travail comme une extension de celui que l'on peut trouver en suivant ce lien.