Développement des systèmes informatiques
LD-relations : étude de cas
Problème :
Écrire un programme qui trouve le maximum de deux valeurs stockées dans deux variables.
Discussion:
- La structure de données de ce programme contiendra trois variables de type int, dénotées par nous par a, b et max.
- Nous exigerons que les valeurs finales de a et b soient les mêmes que les valeurs initiales.
- Remarquons que la valeur initiale de max (c.-à-d. ‘max) n’est pas pertinente.
Cette discussion mène à la spécification suivante du programme à l’aide d’une relation LD, Ls = (Rs, Cs) :
- Dom(Rs) est un ensemble de triplets ordonnés d’entiers (valeurs initiales de a, b et max)
- Image(Rs) est un ensemble de triplets ordonnés d’entiers (valeurs finales de a, b et max)
- Cs = Dom(Rs)
- ((‘a, ‘b, ‘max), (a’, b’, max’)) ∈ Rs ⇔
(a’ = ‘a) ∧ (b’ = ‘b) ∧
((‘a ≤ ‘b) ⇒ (max’ = ‘b)) ∧
((‘a ≥ ‘b) ⇒ (max’ = ‘a))
Représentation tabulaire du prédicat caractéristique de Rs
| T1 | 'a ≤ 'b | 'a ≥ 'b |
| a' = | 'a | 'a |
| b' = | 'b | 'b |
| max' = | 'b | 'a |
- Pour faciliter la vérification de tables nous exigerons que les conditions qui entêtent les colonnes soient mutuellement exclusives. Dans la dernière table nous devons donc remplacer l’opérateur "≤" par "<" ou bien "≥" par ">".
| T2 | 'a ≤ 'b | 'a > 'b |
| a' = | 'a | 'a |
| b' = | 'b | 'b |
| max' = | 'b | 'a |
-
Les deux premières lignes de T2 peuvent être présentées dans la notation standard ce qui donne l’expression suivante :
(a’ = ‘a) ∧ (b’ = ‘b) ∧
| T3 | 'a ≤ 'b | 'a > 'b |
| max' = | 'b | 'a |
- Les deux conditions dans T3 peuvent être représentées sous forme différente (utile dans le cas d’expressions longues - la table plus serrée et plus facile à utiliser) :
| T4 | ('a ≤ 'b) = |
| true | false |
| max' = | 'b | 'a |
- Encore une autre forme :
- L’opérateur d’égalité (dans la valeur "après") peut être remplacé par n’importe quel opérateur relationnel ou par la barre verticale "|". Cette dernière est lue "telle que" et les entrées dans la ligne correspondante doivent être des prédicats. Par exemple, la dernière ligne dans T5 pourrait être réécrite comme suit :
