Département d'Informatique
Maîtrise d'Informatique 2001/2002
Spécifications formelles, preuves
& construction de programmes
Travaux dirigés
Lundi 7 janvier 2002


Sémantique d'un module en CafeOBJ:
Σ-algèbres et modèles




Exercice 1 : Le module LISTE
Soit Σ, la signature suivante donnée en CafeOBJ:

  signature {
    using(NAT)
    [ Liste ]                        

    op liste-vide : -> Liste
    op adjt__ : Nat Liste -> Liste
    op tete_ : Liste -> Nat
    op queue_ : Liste -> Liste
    op longueur_ : Liste -> Nat
  }
  1. Donner une Σ-algèbre évidente. Soit Liste, cette algèbre.
  2. Proposer une autre Σ-algèbre moins évidente, qui associe à la sorte Liste, l'ensemble des listes d'entiers positifs ou nuls, de longueur inférieure ou égale à 3 éléments. Soit Liste3, cette autre Σ-algèbre.
  3. Donner des exemples de termes de l'algèbre des termes clos, notée TΣ.
    Même question pour l'algèbre des termes, notée T(Σ,X), où X est un ensemble (non vide) de variables.
  4. Dans l'algèbre Liste3 que vaut adjt (s 0) (adjt 0 (adjt 0 (adjt 0 liste-vide))) ?
    Qu'en est-il de tete (adjt (s 0) (adjt 0 (adjt 0 (adjt 0 liste-vide)))) ?


Exercice 2 : Le module LISTE (suite)
On complète le module en écrivant: 

module LISTE {
  ...
  axioms {
   var n : Nat
   var l : Liste

   eq longueur liste-vide = 0 .
   eq longueur (adjt n l) = s (longueur l) .

   eq tete  (adjt n l) = n .
   eq queue (adjt n l) = l .
  }
}
  1. Est-ce que Liste3 est un modèle de la spécification (Σ, E), définie par la signature Σ de l'exercice 1 et par l'ensemble d'équations E ci-dessus ? Même question pour Liste.

  2. Vérifier que Liste est un modèle initial de la spécification (Σ, E) ; i.e., montrer un isomorphisme entre Liste et le modèle initial obtenu à partir de l'algèbre des termes quotientée par les axiomes.


Exercice 3 : le module SITUATION-FAMILIALE
Considérons le module suivant:

module SITUATION-FAMILIALE {
  protecting(BOOL)
  signature {
    [ Etat ]                        

   op célibataire : -> Etat
   op veuf        : -> Etat
   op marié       : -> Etat

   op sit-diff : Etat Etat -> Bool 
  }   

  axioms {
   var x : Etat 
   eq sit-diff(x,x) = false .
   eq sit-diff(célibataire,marié) = true .
  }
}
  1. Donner un modèle initial de ce module, un modèle qui ne soit pas initial, et une algèbre qui ne soit pas un modèle.

  2. quel axiome ajouter pour que dans tout modèle, la relation sit-diff soit symétrique ?

  3. Trouver un axiome tel que tout modèle initial qui satisfait cet axiome satisfasse forcément les trois axiomes précédents.


This document was translated from LATEX by HEVEA.