Planche 1
Cours 5
Mémoire--bis
Jean-Jacques.Levy@inria.fr
http://jeanjacqueslevy.net

secrétariat de l'enseignement:
Catherine Bensoussan
cb@lix.polytechnique.fr
Laboratoire d'Informatique de l'X
Aile 00, LIX
tel: 34 67
http://w3.edu.polytechnique.fr/informatique

Planche 2
Références
Planche 3
Plan

  1. Complexité de l'inférence de type de PCF
  2. Typage des références
  3. Variables modifiables
  4. L-values et R-values
  5. Assertions de correction
  6. Correction faible, correction forte
  7. Alias
  8. Équivalences de type
Planche 4
Complexité de l'inférence de type de PCF

Mairson a montré qu'elle pouvait être en O(22n). Mais en général elle est quasi linéaire.

Exemple problématique
let  x0 = l x . (x, x) in
let  x1 = l y . x0 (x0  y) in
let  x2 = l y . x1 (x1  y) in
...
let  xn = l y . xn-1 (xn - 1  y) in
xn  (l z . z)

Exercice 1Calculer son type et essayer de comprendre pourquoi il est compliqué.

Planche 5
Typage des références

Le typage polymorphe des références viole le théorème de progression.
let  r = ref nil in r :=
 
3
:: nil; (hd  !r)  
 
2

Il faut donc se souvenir des valeurs stockées dynamiquement dans une référence pour ne pas avoir de contradictions.

Solution 1 Toutes les références sont monomorphes.

Alors ! ou := ne sont plus typables. Mais on peut typer !M et M := N. On ne sait plus aussi typer les variables références polymorphes dans les tris, par exemple.

Solution 2 [Leroy] Dans let  x = M in N, on ne généralise pas les variables de type apparaissant dans le type d'une référence allouée dans l'évaluation de M.

Dans Ocaml, _a désigne une variable de type non généralisable. Par exemple, ref (l x.x)  :  ref(_a ® _a).

Planche 6
Variables modifiables

Termes
M, N, P ::= ... voir cours précédents
  | letvar x ¬ M in N création
  | x valeur
  | x ¬ M modification de valeur

Exemples

letvar c ¬ 0 in let  x = c ¬ c + 1 in c
letvar c ¬ 0 in let  f = (l x. let  y = c ¬ c + 1 in x) in f(4) + f(5) + c
letvar c ¬ 0 in let  f = (l x.let  y = c in let  z = c ¬ x in y) in f(2) + f(3)

letvar c ¬ 0 in c ¬ c + 1; c
letvar c ¬ 0 in let  f = (l x. c ¬ c + 1; x) in f(4) + f(5) + c
letvar c ¬ 0 in let  f = (l x.let  y = c in c ¬ x; y) in f(2) + f(3)

Planche 7
Règles de réductions
allocv á letvar x ¬ V in N,  sñ ® á N[x\!],  s + [=V]ñ (Ïdomain(s))
derefv á !,  sñ ® á s(),  sñ
assign á ! ¬ V,  sñ ® á (),  s[\ V]ñ

On distingue deux sortes d'occurrences d'une variable x modifiable: On peut traduire letvar dans le calcul précédent, en remplacant toute occurence droite d'une variable modifiable x par !x et en changeant toute déclaration letvar x ¬ M in N par let  x = ref M in N.

Exemple:
let  c = ref 0 in c :=  !c + 1;  !c
let  c = ref 0 in let  f = (l x. c :=  !c + 1; x) in f(4) + f(5) +  !c
let  c = ref 0 in let  f = (l x.let  y =  !c in c := x; y) in f(2) + f(3)

Planche 8
Remarque

á M,  sñ ® á M',  s'ñ implique á C[M],  sñ ® á C[M'],  s'ñ si C[ ] ¹ C'[[ ] ¬ N]

Planche 9
Valeur gauche --- Valeur droite

Les variables modifiables standard des langages impératifs ont donc deux types de valeurs possibles: On a aussi ce phénomène avec les éléments de tableaux, puisque dans v[i] ¬ v[i] +1, l'évaluation n'est pas la même des deux cotés de ¬.

Certains langages permettent les appels de paramètre par référence (Fortran, Pascal, C++). Alors c'est la valeur gauche de l'argument qui se substitue au paramètre.

D'autres langages ne les autorise pas, car trouvant l'écriture dangereuse (C, Java, ML).

Exercice (difficile) Rajouter les paramètres par référence à PCF.
Planche 10
Exemple

Considérons le calcul itératif suivant des nombres de Fibonacci.

ifz  n then x ¬ 0 else
letvar  y ¬ 0 in
x ¬ 1;
letvar  k ¬ 1 in
while  k ¹ n do
let  t = y in (
y ¬ x;
x ¬ x + t;
k ¬ k + 1)

On veut montrer que n ³ 0 au début de ce programme implique x = fib (n) à la fin.

Planche 11
Assertions

{n ³ 0}
ifz n then x ¬ 0 else
{n > 0 Ù x = 0}
letvar y ¬ 0 in
x ¬ 1;
{n > 0Ù x = fib (1)Ù y = fib  (0)}
letvar k ¬ 1 in
{k £ nÙ x = fib (k)Ù y = fib  (k-1)}
while k ¹ n do
{k < nÙ x = fib (k)Ù y = fib  (k-1)}
let  t = y in (
{k < nÙ x = fib (k)Ù y = fib  (k-1) Ù t = fib  (k-1) }
y ¬ x;
{k < nÙ x = fib (k)Ù y = fib  (k) Ù t = fib  (k-1) }
x ¬ x + t;
{k < nÙ x = fib (k+1)Ù y = fib  (k) Ù t = fib  (k-1) }
k ¬ k + 1)
{x = fib (n)}

Planche 12
Invariants de boucle

{n ³ 0}
ifz n then x ¬ 0 else
{n > 0 Ù x = 0}
letvar y ¬ 0 in
x ¬ 1;
{n > 0Ù x = fib (1)Ù y = fib  (0)}
letvar k ¬ 1 in
{k £ nÙ x = fib (k)Ù y = fib  (k-1)}
while k ¹ n do
{k < nÙ x = fib (k)Ù y = fib  (k-1)}
let  t = y in (
{k < nÙ x = fib (k)Ù y = fib  (k-1) Ù t = fib  (k-1) }
y ¬ x;
{k < nÙ x = fib (k)Ù y = fib  (k) Ù t = fib  (k-1) }
x ¬ x + t;
{k < nÙ x = fib (k+1)Ù y = fib  (k) Ù t = fib  (k-1) }
k ¬ k + 1)
{x = fib (n)}

Planche 13
Méthode des assertions [Floyd, Manna]

On a placé des assertions logiques en divers points du programme à vérifier quand le contrôle passe en ce point. Certains langages (Caml) permettent l'écriture de telles assertions, et l'interpréteur lève une exception si l'assertion est fausse.

Les assertions peuvent aussi se démontrer statiquement, avant que le programme ne s'exécute. Il faut alors faire une preuve dans un système logique contenant des formules du genre
|-{P} M {Q}
où P et Q sont deux prédicats et M un terme de programme.

Cette formule est vraie si P(s) et á M,  sñ ®* á V,  s'ñ impliquent P(s'). Autrement dit, si la pré-condition P est vraie avant l'exécution de M, et si M termine, la post-condition Q est vraie après l'exécution de M.

Planche 14
Logique de Floyd-Hoare
|-{P[x\ M]}  x¬ M  {P}
|-PÉ P'    |- {P'}  M  {Q'}   |- Q'É Q
|-{P}  M  {Q}
|-{P}  M  {Q}    |-{Q}  N  {R}
|-{P}  M;N  {R}
|-{P Ù Q}  N  {P}
|-{P}  while Q do N  {P Ù ¬ Q}
|-{P Ù R}  M  {Q}    |-{P Ù ¬ R}  N  {Q}
|-{P}  if  R then M else N  {Q}
|-{P}  ()  {P}
|-{P}  x ¬ M; N  {Q}    (x ÏFV(P) È FV(Q))
|-{P}  letvar x ¬ M in N  {Q}
|-{P}  M  {P'}    |-{Q}  M  {Q'}
|-{P Ù Q}  M  {P' Ù Q'}
|-{P}  M  {P'}    |- {Q}  M  {Q'}
|-{P Ú Q}  M  {P' Ú Q'}

Exercice Se servir de la logique ainsi décrite pour faire rigoureusement la preuve de correction du calcul de Fibonacci.

Planche 15
Correction partielle -- Correction totale

Il n'est pas question de faire ici un cours sur la vérification (cf. DEA Sémantique, Preuve et Programmation).
(1) |-{x £ 10}  while x ¹ 10 do x ¬ x + 1  {x = 10}
(2) |-{vrai }  while x ¹ 10 do x ¬ x + 1  {x = 10}
(3) |-{x > 10}  while x ¹ 10 do x ¬ x + 1  {faux }

(1) est fortement (totalement) correct,
(2) et (3) sont partiellement corrects

La pré-condition de (1) garantit la terminaison.

Chaque fois que l'on a une difficulté avec un morceau de programme critique, il est bon d'écrire formellement les assertions à vérifier. Faire la preuve mécaniquement est beaucoup plus difficile. Programmes zéro-fautes.

Planche 16
Alias

Deux références x et y sont deux alias dans un état mémoire s ssi s(x) = = s(y). Par exemple

let  x = ref 4 in
let  y = x in
x := 3;
!y

Dans un langage sans références explicites, les alias sont plus difficiles à détecter

letvar x ¬ 4 in
let  y = x in
x := 3;
y

Les alias existent aussi avec les éléments de tableaux. Par v[i] est un alias de v[j] quand i = j.

En Pascal, ca se complique avec les paramètres par référence. En C, c'est aussi assez complexe puisqu'on peut prendre l'adresse de tout objet. En C++, on peut faire les deux!!

Planche 17
Détection d'alias

Trouver les alias, ou prouver leur inexistence, permet de détecter des modules indépendants. Important pour
Planche 18
En TD -- la suite A la maison et prochaine fois

This document was translated from LATEX by HEVEA.