L'objectif de ce TP est d'étendre l'interprète du langage A6000 aux nouvelles constructions introduites dans les TP 5 et 6.

1. Sémantique

On reprend les définitions utilisées dans le cours d'ouverture, étendues au système complet.

1.1. Jugements

Les valeurs sont de l'une des deux formes suivantes :

L'environnement ρ est une fonction qui à une variable associe une valeur. Le tas θ est une fonction qui à une adresse associe une suite de valeurs (qui représentent les valeurs du tableau à cette adresse).

La sémantique ρ, θ, e ⟹ v, θ' d'une expression e décrit la valeur v résultant de l'évaluation de l'expression e dans l'environnement ρ et avec le tas θ, ainsi que le tas θ' tel que cette évaluation l'aura éventuellement modifié.

La sémantique ρ, θ, i ⟹ ρ', θ' d'une instruction i décrit l'environnement ρ' et le tas θ' obtenus après exécution de l'instruction i, partant de l'environnement ρ et du tas θ.

1.2. Règles

La sémantique des expressions e est données par les équations suivantes : 

                                       ρ(id) = v
      ------------------         --------------------
      ρ, θ, n  ⟹  n, θ          ρ, θ, id  ⟹  v, θ


      ρ, θ, e₁  ⟹  v₁, θ₁      ρ, θ₁, e₂  ⟹  v₂, θ₂
     --------------------------------------------------
            ρ, θ, e₁ op e₂  ⟹  v₁ ⟦op⟧ v₂, θ₂


      ρ, θ, e₁  ⟹  a, θ₁      ρ, θ₁, e₂  ⟹  i, θ₂      θ₂(a) = v₁...vₙ
     ---------------------------------------------------------------------
                       ρ, θ, e₁[e₂]  ⟹  vᵢ, θ₂


        ρ, θ, e  ⟹  n, θ'      ¬ l ∈ dom(θ)
       --------------------------------------
          ρ, θ, [e]t  ⟹  l, θ{l->0₁...0ₙ}


     ρ, θ, eₙ  ⟹  vₙ, θₙ      ...      ρ, θ₂, e₁  ⟹  v₁, θ₁
     ρ(f) = (x₁,...,xₙ) -> b             
     {x1->v₁,...,xₙ->vₙ,result->?}, θ₁, b  ⟹  ρ', θ'
    -----------------------------------------------------------
            ρ, θ, f(e₁,...,eₙ)  ⟹  ρ'(result), θ'

La sémantique des instructions i et des listes d'instructions b est donnée par les règles d'inférence suivantes : 

                           ρ, θ, i  ⟹  ρᵢ, θᵢ         ρᵢ, θᵢ, b  ⟹  ρ', θ'
  ------------------       --------------------------------------------------
  ρ, θ, ε  ⟹  ρ, θ                      ρ, θ, i;b ⟹ ρ', θ'

			   
           ⟦e⟧ρθ = v, θ'                        ⟦e⟧ρθ = v, θ'
 ---------------------------------      --------------------------[Affiche v]
 ρ, θ, id := e  ⟹  ρ{id ← v}, θ'       ρ, θ, print(e)  ⟹  ρ, θ'

			   
   ⟦e₁⟧ρθ = a, θ₁     ⟦e₂⟧ρθ₁ = i, θ₂     ⟦e⟧ρθ₂ = v, θ'     θ'(a) = v₁..vᵢ..vₙ
   ----------------------------------------------------------------------------
                 ρ, θ, e₁[e₂] := e  ⟹  ρ, θ'{a->v₁..v..vₙ}

			   
                                ⟦e⟧ρθ = ⊥, θ'
                      -------------------------------
                      ρ, θ, while (e) (b)  ⟹  ρ, θ'

			   
 ⟦e⟧ρ₀θ₀ = ⊤      ρ₀, θ₀, b  ⟹  ρ₁, θ₁      ρ₁, θ₁, while (e) (b)  ⟹  ρ₂, θ₂
 ------------------------------------------------------------------------------
                      ρ₀, θ₀, while e (b)  ⟹  ρ₂, θ₂

			   
                 ⟦e⟧ρθ = ⊤, θ'      ρ, θ', b₁  ⟹  ρ₁, θ₁
	        ------------------------------------------
                 ρ, θ, if (e) then b₁ else b₂  ⟹  ρ₁, θ₁

			   
                 ⟦e⟧ρθ = ⊥, θ'      ρ, θ', b₂  ⟹  ρ₂, θ₂
	        ------------------------------------------
                 ρ, θ, if (e) then b₁ else b₂  ⟹  ρ₂, θ₂

			   
     ρ, θ, eₙ  ⟹  vₙ, θₙ      ...      ρ, θ₂, e₁  ⟹  v₁, θ₁
     ρ(f) = (x₁,...,xₙ) -> b             
     {x1->v₁,...,xₙ->vₙ}, θ₁, b  ⟹  ρ', θ'
    -----------------------------------------------------------
                   ρ, θ, f(e₁,...,eₙ)  ⟹  ρ, θ'

2. Travail attendu

Étendre l'interprète du langage A6000 pour qu'il couvre l'ensemble des constructions données dans cette page, en suivant les règles de sémantique.

Plutôt que de représenter explicitement le tas θ, il est possible d'employer les tableaux de Caml. On aurait dans ce cas un shallow embedding du tas et des tableaux.