farescherif / projetlsgit Goto Github PK

### Informations générales : ###

L'objectif de ce projet est de programmer un interpréteur pour un langage impératif simple ainsi 
qu'un prouveur en logique de Hoare pour ce langage impératif.

Pour le langage impératif, nous devons définir les expressions arithmétiques, les expressions 
booléennes et les commandes du langage. 

Pour représenter un triplet de Hoare, il faut représenter une précondition, un programme et une 
postcondition. Les pré et post conditions sont des formules logiques de la mémoire des prédicats.

Ce projet est développé par Farès CHERIF, Thomas FONTENEAU et Maximiliann MARTINS dans le cadre de 
l'unité d'enseignement Logiciels Sûrs au cours du semestre 2 du Master Conception Logicielle de 
l'Université de Poitiers 2021-2022.

### Technologies utilisées : ###

Nous avons choisi le langage Ocaml afin de développer l'interpréteur et le prouveur de Hoare.

### Installation : ###

Vous trouverez dans cette archive, le fichier "aexp.ml" représentant la totalité du code.
Vous pouvez compiler le code par exemple avec l'éditeur Emacs paramétré afin d'ouvrir des 
fichiers Ocaml (.ml).


### Remarque : ###

Chaque partie d’implémentation s’accompagne d’exemples afin de prouver la validité du code et 
de donner des exemples d’utilisation du langage.