You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
Frédéric Bour 7c6ff8db19 Extend logical sequences, begin formalisation of arrays 9 months ago
attic add attic 3 years ago
congre Restructure repository 2 years ago
doc Typos in zml.md 10 months ago
zml Extend logical sequences, begin formalisation of arrays 9 months ago
ztl Minor cleanup 9 months ago
.gitignore Emacs mode 3 years ago
Makefile Typos in zml.md 10 months ago
README.md Correction des liens dans le README 9 months ago
dune-project Emacs mode 3 years ago
zml.opam initial import 3 years ago

README.md

Olive - OCaml Integrated Verification Environment

Organisation du dépôt

  • zml est le projet principal, pour l'instant un mini-ml avec une logique intégrée
  • ztl est une couche au-dessus de Z3 qui offre une API typée et une API pure
  • congre est une implémentation d'un algorithme de congruence closure, adapté au besoin de zml.

Installation

Une fois le dépôt cloné, il faudra installer z3, menhir, pprint et grenier (> 0.12):

opam install z3 menhir pprint grenier

Test

Lancer make depuis le répertoire racine va construire le driver (point d'entrée: zml/bin/main.ml)

Frontend emacs

Le dossier zml/ contient des morceaux d'un mode emacs qui n'est pas du tout à jour, il ne faut pas l'utiliser (en tout cas pour l'instant).