Séance 4
Utilisation de la sémantique du langage Oz

L'objectif de cette séance est d'utiliser la sémantique opérationnelle du langage Oz pour raisonner sur des programmes.

Enoncés des exercices

1. Peloton d'exécution. En utilisant la sémantique formelle du langage, exécutez les deux programmes suivants. Faites attention à l'ordre des instructions dans chacun des cas!

   % Programme 1 local Res in local Arg1 Arg2 in Arg1=7 % 1 Arg2=6 % 2 Res=Arg1*Arg2 % 3 end {Browse Res} end

   % Programme 2 local Res in local Arg1 Arg2 in Arg1=7 % 1 Res=Arg1*Arg2 % 3 Arg2=6 % 2 end {Browse Res} end

   L'environnement de départ est {Browse->browse}. Il mentionne l'identificateur Browse, qui est lié à une variable browse, que nous supposons définie par le système. Par souci de lisibilité, nous écrivons les variables en italique. La pile sémantique initiale pour le programme 1 est donc

       [(local Res in local Arg1 Arg2 in Arg1=7 Arg2=6 Res=Arg1*Arg2 end {Browse Res} end, {Browse->browse})]

   L'effet de l'instruction local est de créer une variable en mémoire, disons res, et d'ajouter l'association Res->res à l'environnement. La pile sémantique devient

       [(local Arg1 Arg2 in Arg1=7 Arg2=6 Res=Arg1*Arg2 end {Browse Res}, {Browse->browse, Res->res})]

   Afin de simplifier l'utilisation de l'environnement, on peut directement remplacer les occurrences libres des identificateurs par la variable qu'ils dénotent. Ce remplacement est permis puisque l'environnement indique précisément que Browse est une notation pour la variable browse. De cette façon, la pile sémantique s'écrit

       [local Arg1 Arg2 in Arg1=7 Arg2=6 res=Arg1*Arg2 end {browse res}]

   La pile sémantique contient maintenant une séquence d'instructions: une instruction local suivie d'un appel à Browse. L'exécution va enlever cette séquence et séparer les instructions sur la pile. Cela donne

       [local Arg1 Arg2 in Arg1=7 Arg2=6 res=Arg1*Arg2 end, {browse res}]

   Comme nous avons simplifié les environnements, il est possible de représenter la pile d'instructions sémantique par une séquence d'instructions sémantiques. De manière très concrète, nous supprimons les délimiteurs de la pile [] et la virgule qui sépare ses éléments, ce qui donne

       local Arg1 Arg2 in Arg1=7 Arg2=6 res=Arg1*Arg2 end {browse res}

   Exécutons maintenant l'instruction local en tête. On crée deux variables en mémoire, disons arg1 et arg2, et nous remplaçons de suite les occurrences libres de Arg1 et Arg2 dans l'instruction local par ces variables.

       arg1=7 arg2=6 res=arg1*arg2 {browse res}

   Les deux instructions en tête de la pile affectent les variables arg1 et arg2. La mémoire contient donc arg1=7, arg2=6 et la pile sémantique devient

       res=arg1*arg2 {browse res}

   Continuez l'exécution du programme, en notant bien ce qui se trouve en mémoire. Ensuite, faites de même pour le programme 2. Quel est précisément l'état final de chaque programme? Qu'affichent-ils chacun? Quelles sont les variables créées par chacun? Que deviennent ces variables lorsque les programmes se terminent?

2. Minimum d'une liste. Considérez le programme ci-dessous, qui définit une fonction MinLoop. L'appel {MinLoop X Ys} renvoie le minimum des éléments de la liste X|Ys.

      local
         fun {MinLoop X Ys}
            case Ys of Y|Yr then
               if Y<X then {MinLoop Y Yr} else {MinLoop X Yr} end
            else X end
         end
      in
         {Browse {MinLoop 7 [5 8 3]}}
      end
   

   Traduisez ce programme en langage noyau, puis exécutez-le en suivant les règles de la sémantique. Pour la traduction en langage noyau, n'oubliez pas que les fonctions sont des procédures, et que le calcul des sous-expressions nécessite l'introduction de variables.

3. Récursion avec construction d'une liste. Soit la fonction Copy définie ci-dessous. Cette fonction renvoie une ``copie'' de la liste passée en argument. Il va de soi que la fonction n'a pas de véritable utilité, nous nous en servons pour étudier sa structure récursive.

      fun {Copy Xs}
         case Xs of X|Xr then X|{Copy Xr} else nil end
      end
   

   Considérons maintenant deux traductions possibles de cette définition de fonction en langage noyau. Dans la traduction 1 à gauche, l'appel récursif {Copy Xr} est exécuté avant de construire la liste avec X. La traduction 2 à droite est une variante. L'unique différence est l'ordre inversé des instructions {Copy Xr Yr} et Ys=X|Yr. Expliquez pourquoi ces deux traductions s'exécutent sans problème.

   % Traduction 1 proc {Copy Xs Ys} case Xs of X|Xr then local Yr in {Copy Xr Yr} Ys=X|Yr end else Ys=nil end end

   % Traduction 2 proc {Copy Xs Ys} case Xs of X|Xr then local Yr in Ys=X|Yr {Copy Xr Yr} end else Ys=nil end end

   Comparons maintenant les deux variantes. Y aura-t-il une différence notable entre les temps d'exécution des deux variantes? Quid de leur utilisation de la mémoire? Quelle variante le compilateur Oz utilise-t-il? A titre de vérification, écrivez un petit programme incluant la définition de la fonction Copy dans l'éditeur oz, et demandez au compilateur sa traduction en langage noyau (menu Oz/Core Syntax).

4. Sémantique et ordre supérieur. Utilisez la sémantique du langage pour déterminer les résultats affichés par le programme ci-dessous. Les fonctions Add1 et Add2 sont définies par le même code, pourquoi renvoient-elles des résultats différents? Expliquez sur base de la sémantique.

      local MakeAdd Add1 Add2 in
         proc {MakeAdd X Add}
            proc {Add Y Z}
               Z=X+Y
            end
         end
         {MakeAdd 1 Add1}
         {MakeAdd 2 Add2}
   
         % {Browse {Add1 42}}
         local V in
            {Add1 42 V} {Browse V}
         end
   
         % {Browse {Add2 42}}
         local V in
            {Add2 42 V} {Browse V}
         end
      end
   

Exercice individuel

Remplissez le formulaire avec vos réponses, ensuite sélectionnez votre tuteur dans la liste. Une fenêtre apparaîtra avec le contenu d'un e-mail que vous devrez envoyer.