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 |
Partager