Introduction

Le but de ce TP est de se familiariser avec le système CafeOBJ.
CafeOBJ fournit une notation pour écrire des spécifications algébriques.
Une spécification algébrique permet de définir formellement un ou plusieurs types et leurs opérations associées
au moyen d'une signature et d'un ensemble d'axiomes.
La signature définit des termes bien formés et chaque axiome est une équation liant 2 termes.
CafeOBJ permet de vérifier l'adéquation de la spécification:
on peut par exemple prouver l'égalité de deux termes en demandant de les réduire
(sous une forme normale) en se servant des axiomes.

Préliminaires
 

• CafeOBJ se trouve sur la machine turing
• CafeOBJ se lance en tapant "cafeobj" et l'on en sort en tapant "q" ou "Ctrl+D"
• en CafeOBJ, une spécification est appelée "module" et porte un nom en majuscules.
• on peut saisir un module de nom M dans un fichier M.mod,
  puis charger ce module dans CafeOBJ avec "input M"
• pour voir le contenu d'un module de nom M, taper "show M"
• certains modules sont prédéfinis comme NAT, INT, RAT, FLOAT et
  BOOL (ce dernier module est par défaut importé dans tout module).
• pour rendre actif un module M (afin de réduire des termes), taper "select M"
• pour réduire un terme t, taper "red t ." (avec un espace entre le terme et le ".").
• pour tester l'égalité ou la différence entre deux termes t1 et t2, taper (resp.) "red t1 == t2 ." ou "red t1 =/= t2 ."
• lorsqu'une réduction tourne mal, le prompt est le suivant "CHAOS>>", pour en sortir et revenir au module précédent, taper ":q"

module LISTE {
  imports {
    using(NAT)
    using(ORDT)
  }
  signature {
    [ Liste ]                       ** listes d'objets de sorte S 

    op listenouv :  -> Liste        ** liste vide           (constructeur)
    op adjt : S Liste -> Liste      ** adjonction est tête  (constructeur)
    op supt : Liste -> Liste        ** suppression en tête  (sélecteur)
    op tête : Liste -> S            ** élément en tête      (sélecteur)
    op vide : Liste -> Bool         ** test de vacuité      (opération externe)
    op lgr  : Liste -> Nat          ** nombre d'éléments    (")
    op _[_] : Liste Nat -> S        ** ième élément         (")
    op lig  : Liste Nat -> Liste    ** sous-liste gauche    (")
    op lid  : Liste Nat -> Liste    ** sous-liste droite    (")
    op conc : Liste Liste -> Liste  ** concaténation        (")
  }
  axioms {
    var x : S
    var l : Liste
    var i : Nat
  
    eq supt(adjt(x,l)) = l .
    eq tête(adjt(x,l)) = x .
    eq vide(listenouv) = true .
    eq vide(adjt(x,l)) = false .

    ...
    eq lig(listenouv,s(i)) = listenouv .
    eq lig(adjt(x,l),s(0)) = adjt(x,listenouv) .  
    eq lig(adjt(x,l),s(s(i))) = adjt(x,lig(l,s(i))) .
    ...
  }
}

Il s'agit de spécifier l'évaluation d'une expression arithmétique sous forme polonaise inversée, à l'aide d'une pile.

On écrira deux modules:

• INT-STACK, qui définit les piles d'entiers,
• puis SYMB-LIST, qui définit les listes de symboles.

la liste de symboles 2, 3, +, 4, *
représente la forme polonaise inversée de l'expression arithmétique 2 3 + 4 *
(ici écrite, justement, sous sa forme polonaise inversée ; la forme standard étant : (2 + 3) * 4).

1. Module INT-STACK
 

      Ecrire un module INT-STACK, avec une sorte IntStack, et les opérations usuelles new (pile vide), pop (dépiler), push (empiler), et top (sommet de la pile).
Tester ce module.

2. Module SYMB-LIST
 

      Ecrire un module SYMB-LIST, avec les sortes Symb et SymbList.
On définira les symboles +, - et *.
On définira une opération <_> : Int -> Symb, qui a pour sens d'associer à un entier sa représentation, à laquelle on prête le statut de symbole.
Pour la définition des listes de symboles, on pourra s'inspirer du mode de construction, et de la notation, des listes en Caml.
Puis définir l'opération eval_ : SymbList -> Int, qui évalue une expression sous forme polonaise inversée, en utilisant une pile d'entiers.
On pourra s'inspirer du mode de fonctionnement de la commande dc de Unix.
Bien vérifier que cela fonctionne.