Projet de Master 1, module: logiciels sûrs.
Création d'un interpréteur pour un langage impératif et un prouveur en logique de Hoare
Langage utilisé: Ocaml
Projet réalisé par Jugurtha ASMA, Hylia BOUDAHBA et Thibault RUCHER
Le dossier projet est composé de plusieurs fichiers .ml: - axpr.ml - bxpr.ml - goal.ml - hoare_triple.ml - prog.ml - projet.ml - tactic.ml - tprop.ml
Testez dans un premier temps le fichier aexpr en faisant CTRL + C + B dans emacs puis faire dans l'ordre suivant: bexpr -> prog -> tprop -> hoare_triple -> goal -> tactic pour que tout compile correctement.