Considérons le langage IMP vu en cours. On rappelle que sa syntaxe est constituée des
true
| false
| a < a′ | not
bskip
| x := a | c ;
c′ | if
b then
c else
c′ | while
b do
cOn définit la notation suivante pour le type des variables :
type var = string
Définir chacune des catégories syntaxiques ci-dessus par des types inductifs nommés aexp
, bexp
et cexp
.
On définit le type state
des états (qui consistent en la valeur courante des variables) par
type state = var -> int
Définir l’état initial state0
(où toutes les variables ont la valeur 0
) ainsi qu’une fonction state_set
de type state -> var -> int -> state
qui modifie la valeur d’une variable dans un état.
Définir des fonctions aeval
, beval
et eval
qui donnent le résultat de l’évaluation de chacune des catégories syntaxiques dans un état donné.
Programmez la fonction factorielle et vérifiez que l’on a bien 5! = 120 :
let () =
let s = state_set state0 "x" 5 in
let s = eval s fact in
assert (s "y" = 120)
Programmez une fonction qui, étant donnés deux entiers a et b, calcule le quotient et le reste de la division euclidienne de a par b (vous devriez arriver à reconstituer cet algorithme sans cours ou internet). Vérifiez que pour a = 279 et b = 15 le quotient est 18 et le reste est 9.
Programmez l’algorithme d’Euclide permettant de calculer le plus grand diviseur commun de deux entiers a et b (vous pourrez ajouter l’égalité d’entiers comme primitive au langage si nécessaire). Vérifier que le pgcd de 1071 et 462 est 21.
Nous allons maintenant implémenter la sémantique à petits pas. La réduction d’une expression n’étant pas toujours définie, nous utiliserons des types option
dans les valeurs de retour : None
signifiera que la réduction n’est pas définie.
ared
de type state -> aexpr -> aexpr option
qui calcule un pas de réduction d’une expression arithmétique.bred
de type state -> bexpr -> bexpr option
qui calcule un pas de réduction d’une expression booléenne.red
de type state -> cexpr -> (state * cexpr) option
qui calcule un pas de réduction d’une commande.red
, la fonction eval
de type state -> cexpr -> state
qui évalue une commande. Vérifier qu’elle fonctionne en testant à nouveau la factorielle (et les autres exemples de la section précédente).