Interface for Module

Le but est d'avoir un moyen de cacher une implémentation derrière une interface plus simple et plus approprié pour la preuve.

En résumé:

1. Verification avec un clone
   • Seulement pour les fonctions de même nom:
     • On ajoute toutes les post-conditions de l'interface
     • On prend les préconditions de l'interface, s'il n'y en a pas
2. Barrière d'abstraction

Plan d'action:

1. Pas d'interface multiple Si nécessaire encoder à la main les interfaces multiples avec clone (dans le cas où il n'y a pas les même fonctions)
2. Utiliser un nom généré, l'utilisateur écrit

      module I type t = a end
      module J : I type t = b end

Le code suivant est généré.

       module J'impl type t = b ; clone I with type t = t end
       module J clone I end

3. Lors de l'extraction et interprétation, copie les modules et applique une substitution (use J -> use J'impl)
4. clone J with ... is only allowed to instantiate symbols that are refinable both in I and J. During extraction/execution this is replaced with clone J'impl with .... We should make an effort to check that the instantiation is valid for the implementation at an early stage, so that we never fail during the extraction.