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.