[Méthode B] Un sac de billes...

Un sac de billes...

Bonjour,

Ci-dessous 3 machines qui modélisent le remplissage et le vidage
d'un ensemble qui représente un sac de billes depuis la machine abstraite
jusqu'à l'implémentation. Tout fonctionne bien avec proB mais il reste 8
obligations de preuve à décharger dans l'implémentation dont certaines avec un but sous la forme
de "il existe ...".

MACHINE
SacDeBille

VARIABLES
sac,nombreBille
INVARIANT
sac <: (0..5) &
nombreBille : NAT &
nombreBille = card(sac)
INITIALISATION
sac := {} ||
nombreBille := 0
OPERATIONS
REMPLIR_SAC =
BEGIN
ANY bille WHERE
bille : (0..5)-sac &
nombreBille + 1 : NAT
THEN
sac := sac \/ {bille} ||
nombreBille := nombreBille + 1
END
END;

VIDER_SAC =
BEGIN
ANY bille WHERE
bille : (0..5) &
bille : sac &
nombreBille - 1 : NAT
THEN
sac := sac - {bille} ||
nombreBille := nombreBille - 1
END
END;

nBilleSac <-- LIRE_NOMBRE_BILLE =
BEGIN
nBilleSac := nombreBille
END

END

REFINEMENT
SacDeBille_r
REFINES
SacDeBille

ABSTRACT_VARIABLES
TableauSac
CONCRETE_VARIABLES
nombreBille

INVARIANT
TableauSac : (0..5) --> BOOL &
sac = TableauSac~[{TRUE}]
INITIALISATION
TableauSac := (0..5) * {FALSE} ||
nombreBille:=0
OPERATIONS
REMPLIR_SAC =
BEGIN
ANY bille
WHERE
bille : (0..5) &
TableauSac(bille) = FALSE &
nombreBille + 1 : NAT
THEN
TableauSac(bille) := TRUE ||
nombreBille := nombreBille + 1
END
END
;

VIDER_SAC =
BEGIN
ANY bille
WHERE
bille : (0..5) &
TableauSac(bille) = TRUE &
nombreBille - 1 : NAT
THEN
TableauSac(bille) := FALSE ||
nombreBille := nombreBille - 1
END
END;

nBilleSac <-- LIRE_NOMBRE_BILLE =
BEGIN
nBilleSac := nombreBille
END

END

IMPLEMENTATION
SacDeBille_i
REFINES
SacDeBille_r
CONCRETE_VARIABLES
TableauSac
INVARIANT
nombreBille : 0..6
INITIALISATION
TableauSac := (0..5) * { FALSE };
nombreBille := 0

OPERATIONS
REMPLIR_SAC =
BEGIN
VAR ii,trouve IN
ii := -1;
trouve:=FALSE;
WHILE ii<5 & trouve=FALSE DO
ii:=ii+1;
VAR nBille IN
nBille := TableauSac(ii);
IF nBille = FALSE THEN
trouve := TRUE
END
END
INVARIANT
ii : (-1..5) &
trouve = bool(FALSE: ran(0..ii<|TableauSac))
VARIANT
5-ii
END;
IF trouve = TRUE THEN
TableauSac(ii) := TRUE;
nombreBille := nombreBille + 1
END
END

END;

VIDER_SAC =
BEGIN
VAR ii,trouve IN
ii := -1;
trouve:=FALSE;
WHILE ii< 5 & trouve=FALSE DO
ii:=ii+1;
VAR bille IN
bille := TableauSac(ii);
IF bille = TRUE THEN
trouve := TRUE
END
END
INVARIANT
ii : (-1..5) &
trouve = bool(TRUE: ran(0..ii<|TableauSac))
VARIANT
5-ii
END;
IF trouve = TRUE THEN
TableauSac(ii) := FALSE;
nombreBille := nombreBille -1
END
END
END;

nBilleSac <-- LIRE_NOMBRE_BILLE =
BEGIN
nBilleSac := nombreBille
END

END

Bonjour,

Je n'ai pas regardé les obligations de preuve.
La spécification peut être simplifiée car la variable nombreBille n'est pas nécessaire car elle est toujours égale à card(sac).
Ci-dessous ma suggestion pour la machine:
Code:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 MACHINE SacDeBille CONSTANTS SAC PROPERTIES SAC = 0..5 ABSTRACT_VARIABLES sac INVARIANT sac <: SAC INITIALISATION sac := {} OPERATIONS REMPLIR_SAC = BEGIN ANY bille WHERE bille : SAC-sac THEN sac := sac \/ {bille} END END; VIDER_SAC = BEGIN ANY bille WHERE bille : sac THEN sac := sac - {bille} END END; nBilleSac <-- LIRE_NOMBRE_BILLE = BEGIN nBilleSac := card(sac) END END

Bonjour M. Lecomte,

Merci pour votre réponse, effectivement çà simplifie les choses mais
j'ai au niveau de la première machine l'obligation de preuve suivante:

"Well definedness" => sac: FIN(sac)

idem au niveau du raffinement.
Au niveau de l'implémentation j'ai 20 obligations de preuve non-prouvées.

J'ai remis à jour les 3 machines ci-après:

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
MACHINE
    SacDeBille

VARIABLES
    sac
CONSTANTS
    SAC
PROPERTIES
    SAC = (0..5)
INVARIANT
    sac <: SAC
INITIALISATION
    sac := {}
OPERATIONS
    REMPLIR_SAC =
    BEGIN
    	ANY bille WHERE
    		bille : SAC-sac
    	THEN
    	    sac := sac \/ {bille}
    	END
    END;
    
    VIDER_SAC = 
    BEGIN
         ANY bille WHERE
             bille : sac
         THEN
             sac := sac - {bille} 
         END
     END;
     
     nBilleSac <-- LIRE_NOMBRE_BILLE =
     BEGIN
         nBilleSac := card(sac)
     END
     
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
REFINEMENT
   SacDeBille_r
REFINES
   SacDeBille

ABSTRACT_VARIABLES
   TableauSac
   
INVARIANT
    TableauSac : SAC --> BOOL &
    sac = TableauSac~[{TRUE}]
INITIALISATION
   TableauSac := SAC * {FALSE} 
OPERATIONS
   REMPLIR_SAC =
   BEGIN
       ANY bille
       WHERE
           bille : SAC &
           TableauSac(bille) = FALSE
       THEN
           TableauSac(bille) := TRUE
       END
   END
   ;

   VIDER_SAC =
   BEGIN
       ANY bille
       WHERE
           bille : SAC &
           TableauSac(bille) = TRUE
       THEN
           TableauSac(bille) := FALSE
       END
   END;
   
    nBilleSac <-- LIRE_NOMBRE_BILLE =
    BEGIN
     nBilleSac := card(TableauSac~[{TRUE}])
    END
    
END

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
IMPLEMENTATION
   SacDeBille_i
REFINES
   SacDeBille_r
VALUES
   SAC=(0..5) 
CONCRETE_VARIABLES
   TableauSac
INITIALISATION
   TableauSac := SAC * { FALSE }
OPERATIONS
   REMPLIR_SAC =
   BEGIN
       VAR ii,trouve IN
           ii := -1;
           trouve:=FALSE;
           WHILE ii<5 & trouve=FALSE DO
               ii:=ii+1;
               VAR nBille IN
                   nBille := TableauSac(ii);
                   IF nBille = FALSE THEN
                      trouve := TRUE                      
                  END
              END
           INVARIANT
               ii : (-1..5) &
               trouve = bool(FALSE: ran(0..ii<|TableauSac))
           VARIANT
               5-ii
           END;
           IF trouve = TRUE THEN
               TableauSac(ii) := TRUE
           END
       END
  
   END;

   VIDER_SAC =
   BEGIN
       VAR ii,trouve IN
           ii := -1;
           trouve:=FALSE;
           WHILE ii< 5 & trouve=FALSE DO
               ii:=ii+1;
               VAR bille IN
                   bille := TableauSac(ii);
                   IF bille = TRUE THEN
                      trouve := TRUE
                  END
              END
           INVARIANT
               ii : (-1..5) &
               trouve = bool(FALSE: ran(0..ii<|TableauSac))
           VARIANT
               5-ii
           END;
           IF trouve = TRUE THEN 
               TableauSac(ii) := FALSE
           END
       END
   END;
   
   nBilleSac <-- LIRE_NOMBRE_BILLE =
   BEGIN
        nBilleSac:=0;
        VAR ii,trouve IN
           ii := -1;
           trouve:=FALSE;
           WHILE ii< 5 DO
               ii:=ii+1;
               VAR bille IN
                   bille := TableauSac(ii);
                   IF bille = TRUE THEN
                      nBilleSac := nBilleSac +1
                  END
              END
           INVARIANT
               ii : (-1..5) &
               nBilleSac = card((0..ii<|TableauSac)~[{TRUE}])
           VARIANT
               5-ii
           END
       END      
   END
   


END

Votre spécification ne correspond pas à votre implémentation.
L'opération REMPLIR_SAC est exprimée sous la forme: ANY x WHERE P(x) THEN S END
Cette substitution est non-déterministe mais elle requiert qu'il y ait au moins un x qui vérifie P(x). Ici il s'agit de trouver une bille dans un sac qui peut être vide.
L'implémentation par contre peut trouver ou ne pas trouver de bille.

Soit votre composant SacDeBille est votre modèle de plus haut niveau et dans ce cas, il faut traiter le cas où il reste au moins une bille et on l'utilise, et le cas où il n'y en a plus et on ne fait rien.
Si le composant SacDeBille est utilisé par un autre composant par importation, dans ce cas l'opération peut être préconditionnée avec not(SAC-sac={})

Côté preuve, sac: FIN(sac) se prouve automatiquement en force 1.