LD-relations

États sûrs

• Un programme est un texte décrivant un ensemble de séquences de changements d’états dans un automate à états finis.
• Chaque séquence est appelée une exécution du programme.
• Soit P un programme et e(P,s₁) une séquence de changements d’états décrite par P et qui commence dans l’état s₁.
  • Une exécution finie est dénotée par e(P, s₁) = <s₁, ..., s_n> et une exécution infinie par e(P, s₁) = <s₁, s₂, ...>.
  • Pour tout e(P, s₁) l’état s₁ est appelé l’état de départ d’une exécution de P.
• Si e(P, s₁) = <s₁, ..., s_n> alors nous disons que cette exécution se termine (ou simplement que ce programme se termine) et s_n est appelé l’état final ou l’état d’arrêt.
• Si pour un état donné s, chaque e(P,s) se termine alors s est appelé un état sûr pour P; l’ensemble d’états sûrs est dénoté par S_P.

LD-Relations ("limited domain relations")

• Si nous ne sommes pas intéressés dans des états intermédiaires d’exécution alors chaque programme déterministe qui se termine peut être décrit par une fonction de programme, c.-à-d. une fonction dont le domaine est un ensemble d’états sûrs et dont l’image est un ensemble d’états finaux.
• Des programmes non-déterministes ne peuvent pas être décrits complètement par des fonctions programme.
  • un programme qui a commencé dans un état sûr peut se terminer dans un ou plusieurs états finaux; une relation doit donc être utilisée au lieu d’une fonction.
  • un programme qui a commencé dans un état donné peut dans certains cas se terminer et dans d’autres cas non; une relation classique sur un ensemble d’états n’est donc pas suffisante pour décrire tous les cas relevants.
• En 1983 D.Parnas a suggéré la solution suivante au dernier problème : au lieu d’utiliser une relation nous devrions utiliser un couple (relation, ensemble). Cet ensemble fournit l’information supplémentaire nécessaire.
• Une LD-relation est un couple ordonné L = (R_L, C_L) où
  • R_L est une relation,
  • C_L est un ensemble tel que C_L ⊆ Dom(R_L); il est appelé l’ensemble de compétence de L.
• Nous pouvons utiliser une LD-relation pour décrire un programme comme suit : soit P un programme, x et y des états, L_P = (R_P, C_P) une LD-relation tels que :
  • (x,y) ∈ R ⇔ ∃e(P,x) [e(P,x) ∈ Exec(P,X_P) ∧ e(P,x) = <x,...,y>],
  • x ∈ C_P ⇔ x ∈ S_P
  L_P est appelé une LD-relation de programme P

• Notons que si x n’est pas dans le domaine de R alors chaque e(P,x) est infinie, c.-à.-d. P qui commence dans x ne se terminera jamais.
• Si C_P = Dom(R_P) alors, par convention, l’ensemble de compétence peut être omis. Autrement dit, l’ensemble de compétence par défaut est Dom(R_P).
• Si le programme est déterministe alors la composante relationnelle d’une LD-relation est la même que la fonction de programme. Soit F_P la fonction de programme; alors
  • F_P = R_P
  • Dom(F_P) = S_P = C_P
• Une LD-relation peut être aussi utilisée comme spécification de programme.
• En général, un programme peut être spécifié par un ensemble de LD-relations. Soit P un programme, L_P = (R_P, C_P) sa LD-relation, S un ensemble de LD-relations et soit L_S ∈ S, L_S = (R_S,C_S). Alors
  • programme P satisfait une LD-relation L_S ⇔ (C_S ⊆ C_P) ∧ (R_P ⊆ R_S)

Exemple 1

Programme P :

int i,j;
...
while (i!=0) i=j;

LP = (RP, CP)
CP = {(i,j) | i=0 ∨ j=0}
RP = {(('i,'j),(i',j')) | i' = 0 ∧ j' = 'j}

Exemple 2

Programme P :

int i;
...
while (i<0) i++;

LP = (RP, CP)
CP = { i | true }         // l'univers
RP = {('i,i') | 'i ≤ 0 ∧ i' = 0 ∨ 'i > 0 ∧ i' = 'i}

Exemple 3

Programme P :

int i,j;
...
if (i<0) {
  Random rand = new Random();
  j = rand.nextInt();
  if (j == 13)
    while (true) i = 100;
  else
    j = 12;
} else
  j = 50;

LD-relation :

LP = (RP, CP)
CP = {(i,j) | i ≥ 0}
RP = {(('i,'j),(i',j')) | 'i ≥ 0 ∧ i' = 'i ∧ j' = 50}

Exemple 4

LD-relation :

LP = (RP, CP)
CP = {x | true}
RP = {('x,x') | x' ≥ 0 }

Programme P :

int i;
...
i = 1023;

Exercice

Pour chacun des programmes ci-dessous écrivez :

• une expression booléenne décrivant le domaine de la fonction de programme correspondante
• une expression booléenne décrivant l’image de la fonction de programme correspondante

Vous pouvez présumer qu’il n’y a pas de restriction sur l’ensemble des entiers qui peuvent être représentés (même si cette supposition n’est pas réaliste). Vous pouvez présumer que l’état est défini entièrement par les valeurs des variables x et y.

(1) while (true) x = y

Domaine:

Image:

(2) while (x < 20) x = y

Domaine:

Image:

(3) while (x < 20) x++

Domaine:

Image:

(4) while (x < 20) x--

Domaine:

Image:

(5) while (x != 20) x = x + 2

Domaine:

Image:

Composition de fonctions de programme

Exercice

Soit int x,y,z;

La fonction de programme du programme A est la suivante :

x' ='x + 1 ∧ y' = 'y ∧ z' = 'z

et la fonction de programme du programme B est comme suit :

Trouvez la fonction de programme des programmes suivants :

1. A;B
   
   
   
2. B;A