Constats, contraintes, invariant

Prenons cette phrase en langage naturel : "Certains a sont b"

Supposons que :

SETS
TRUC
VARIABLES
a, b
INVARIANT
a <: TRUC & b <: TRUC

"Certains a sont b" peut se lire comme

• un fait : on constate que certains a sont b. Cela ne veut pas dire qu'il est obligatoire que certains a soient b, qu'ils le seront tout le temps, qu'il l'ont été dans le passé. On peut écrire que l'on constate que # x . x : a & x :b, il existe au moins un a qui est aussi un b. Comme on a écrit "certains", on peut même écrire # s. s <:a & card(s) >1 & s <: b, ce qui exprimer qu'il y a plus d'un a qui est b.

Mais on ne mettra pas ces prédicats dans l'INVARIANT car il ne s'agit que d'un constat et non d'une loi, d'une obligation, d'une contrainte.
Bien sûr, notre invariant actuel permet tout à fait que #1 x . x : a & x :b

• une contrainte, une obligation, une loi : il faut que certains a soient b. Par exemple, il faut qu'un Français soit chef de l'Etat à tout moment. La Constitution prévoit cela. Si un Pdt de la République meurt en exercice, il est immédiatement remplacé par le Pdt du Sénat (en termes de B, une seule opération avec deux substitutions parallèles).

Dans ce cas, on mettra nos prédicats dans l'invariant.

Ce qu'on vient de dire pour le "il existe" est aussi valable pour le "pour tous".


Vous avez bien compris ?

Alors vous avez compris que si

r1 = A -->B &
r2 = A <-->B

alors r1 <: r2 que si r1 = A +-> B &
r2 = A -->B

alors r2 <: r1 L'ensemble de toutes les fonctions totales de A vers B est inclus dans l'ensemble de toutes les fonctions partielles de B vers A. J'ai pu avoir hier constaté que tout A était lié à un et un seul B, sans pour cela avoir eu une loi obligeant tous les A à être liés à un et un seul B. J'ai alors spécifié dans mon invariant une fonction partielle (et non une fonction totale). Quand on fait l'INITIALISATION en B, on donne une valeur aux variables. On peut très bien donner une fonction totale pour initialiser une variable dont l'invariant dit que ce doit être une fonction partielle.
De le même façon, si j'ai déclaré :

SETS
ETUDIANT
VARIABLES
fumistes, mesEtudiants
INVARIANT
fumistes <: ETUDIANT &
mesEtudiants <: ETUDIANTS &

Je peux initialiser fumistes et mesEtudiants par le même sous-ensemble d'ETUDIANT, dont l'ensemble vide. MAIS mon invariant ne dit pas que tous mesEtudiants sont des fumistes.

La preuve de mon initialisation montrera que je peux au moins avoir une instanciation de mes variables qui respecte l'invariant. Que j'ai au moins un MODELE. Mais j'espère bien que jamais cela ne se réalisera .

Lire aussi sur un sujet proche