Introduction

Le but de ce TP est de montrer que CafeOBJ permet de vérifier l'implantation d'un type de données abstrait (ici, les multi-ensembles)
par un autre type de données (ici, les tableaux) plus concret, c'est-à-dire plus proche de la représentation en mémoire.
CafeOBJ permet de vérifier la correction de l'implantation.

Quelques commandes utiles
 

• "open M" permet d'ouvrir le module de nom M dans le but de démontrer certaines propriétés des opérations définies dans ce module.
  "open" permet en plus de "select" de définir de nouvelles opérations, de nouvelles variables ou de nouveaux axiomes
  uniquement pour les besoins d'une démonstration.
  
• "op x : -> S ." (après avoir ouvert un module par "open") définit un élément x de sorte S.
  
• "eq t = t' ." (après avoir ouvert un module par "open") ajoute un nouvel axiome.
   Cet axiome est à considérer comme une hypothèse vraie pour la suite de la démonstration.
  
• "close" permet de fermer le dernier module ouvert par "open".
  

1. Module INT-MULTISET
 

      On désire spécifier les multi-ensembles.

Informellement, un multi-ensemble est un ensemble qui peut contenir plusieurs fois le même élément.

Voici la définition d'un multi-ensemble :

Un multi-ensemble M d'éléments dans un ensemble E est
une fonction de E vers l'ensemble des entiers naturels,
qui fait correspondre à chaque élément x de E,
le nombre M(x) d'occurrences de x dans M.

Exemple - Un exemple de multi-ensemble est { 1 , 2 , 3 , 3 } (ici noté en extension entre à la manière des ensembles) qui contient 4 éléments et 2 fois l'élément 3.

Pour la suite, on considère les multi-ensembles d'éléments dans Z (l'ensemble des entiers relatifs).

Ecrire un module INT-MULTISET, avec une sorte IntMultiset pour l'ensemble des multi-ensembles dont les éléments sont des entiers relatifs,
une opération occur qui retourne le nombre d'occurrences d'un entier dans un multi-ensemble,
et les opérations caractéristiques des multi-ensembles: in (appartenance), union (union de 2 multi-ensembles), diffe (différence).

Tester ce module.

2. Module INT-ARRAY
 

      Ecrire un module INT-ARRAY, avec la sorte IntArray pour les tableaux d'entiers relatifs.
On définira les opérations de création d'un tableau de taille donnée, d'accés à l'élément à un indice donné,
de modification d'un tableau en affectant une nouvelle valeur à un élément, et une opération size qui donne la taille d'un tableau.

Bien vérifier que cela fonctionne.

3. Module INT-MS-USING-INT-ARRAY
 

      On cherche maintenant à représenter les multi-ensembles par des tableaux, comme on le ferait dans un langage impératif (C, par exemple).

Tout multi-ensemble de cardinal p inférieur ou égal à n peut être représenté par une structure à 2 champs:
- un tableau de taille n pour stocker les éléments du multi-ensemble et
- un entier (de type Int comme en C) pour stocker le nombre p d'éléments du multi-ensemble.

Ecrire un module INT-MS-USING-INT-ARRAY, avec IntMS pour la sorte des représentations de multi-ensembles.
Définir une opération <_;_> : IntArray Int -> IntMS qui retourne le multi-ensemble représenté par un tableau et un entier.
Redéfinir les opérations multi-ensemblistes en utilisant les opérations sur les tableaux: on nommera occur-t, in-t, union-t et inter-t, ces opérations.

Vérifier que l'implantation des multi-ensembles est correcte.
Pour cela, prendre des cas particuliers de multi-ensembles et montrer que les opérations occur-t, in-t, union-t et diffe-t
implantent bien les opérations multi-ensemblistes.

Réfléchir au moyen de vérifier cela dans le cas général.