Discussion :

[Laurent Guillaume]

Bonjour,

Je tente de modéliser et de prouver un buffer circulaire dans l'Atelier B sous forme d'une suite.
Cette suite est ensuite raffinée sous forme d'un tableau sur lequel pointent
un pointeur de lecture et d'écriture. Les deux machines sont ci-après et sont correctement simulées
dans l'outil proB. Mon problème se situe au niveau des preuves que je n'arrive pas à décharger; soit
mon modèle est faux mais proB montre le contraire à mon sens soit mes invariants sont incorrectes.
Il est possible que tout soit prouvable manuellement mais je ne sais que faire avec les preuves
dont le but est de type "=>bfalse". Le buffer circulaire est souvent utilisé en informatique embarquée
et il serait intéressant de pouvoir le modéliser et de le prouver en B afin d'en générer du code sans bug.

Bon courage !

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
MACHINE
    Mach1
SETS
    DATAS
CONSTANTS
    NoEl,MAX_SIZE
PROPERTIES
    NoEl : DATAS &
    MAX_SIZE : NAT1
VARIABLES
    pile
INVARIANT
    pile : seq(DATAS)
INITIALISATION
    pile := []
OPERATIONS
    nStatus <-- WRITE_TO(el) =
    PRE
        el : DATAS
    THEN
        SELECT size(pile)=MAX_SIZE THEN
            nStatus := FALSE
        ELSE
            nStatus := TRUE ||
            pile := pile<-el
        END
    END;
    
    nStatus,nEl <-- READ_FROM =
    BEGIN
        SELECT size(pile) = 0 THEN
            nStatus := FALSE ||
            nEl :: DATAS
        ELSE
            nStatus := TRUE ||
            nEl := first(pile) ||
            pile := tail(pile)
        END
    END;
    
    nSize <-- GET_SIZE = 
    BEGIN
        nSize := size(pile)
    END
    
    
END


REFINEMENT Mach1_r
REFINES Mach1
DEFINITIONS
    MAX_ARR == (MAX_SIZE+1)
VARIABLES
    arr_vrb,p_read,p_write
INVARIANT
    arr_vrb : 0..MAX_ARR --> DATAS &
    p_read : 1..MAX_ARR &
    p_write : 1..MAX_ARR &
    ((p_write>=p_read)=>(p_write-p_read = size(pile))) &
    ((p_write>=p_read)=>(p_read..p_write-1)<|arr_vrb=pile) &
    ((p_write<p_read)=>(MAX_ARR-p_read+p_write=size(pile))) &
    ((p_write<p_read & p_write=1)=>(((p_read..MAX_ARR)<|arr_vrb))=pile) &
    ((p_write<p_read & p_write/=1)=>(((p_read..MAX_ARR)<|arr_vrb) \/ ((1..p_write-1)<|arr_vrb))=pile)
INITIALISATION
    arr_vrb := (0..MAX_ARR) * {NoEl} ||
    p_read := 1 ||
    p_write := 1
OPERATIONS
    nStatus <-- WRITE_TO(el) =
    PRE
        el : DATAS
    THEN
        SELECT p_write=MAX_ARR THEN
            SELECT p_read = 1 THEN
                nStatus := FALSE
            ELSE
                nStatus := TRUE ||
                arr_vrb(p_write):=el||
                p_write := 1
            END
        ELSE
            SELECT p_write+1 /= p_read THEN
                nStatus := TRUE ||
                arr_vrb(p_write):=el||
                p_write := p_write + 1
            ELSE
                nStatus := FALSE
            END
        END     
    END;

    
    nStatus,nEl <-- READ_FROM =
    BEGIN
        SELECT p_read=MAX_ARR THEN
            SELECT p_write = MAX_ARR THEN
                nStatus := FALSE ||
                nEl := NoEl
            ELSE
                nStatus := TRUE ||
                nEl := arr_vrb(p_read)||
                p_read := 1
            END
        ELSE
            SELECT p_read  /= p_write THEN
                nStatus := TRUE ||
                nEl := arr_vrb(p_read)||
                p_read := p_read + 1
            ELSE
                nStatus := FALSE ||
                nEl := NoEl
            END
        END     
    END;
    
    nSize <-- GET_SIZE = 
    BEGIN
        SELECT p_write>=p_read THEN
            nSize := p_write-p_read
        ELSE
            nSize := MAX_ARR - p_read + p_write
        END

    END
 END

[ThierryLecomte]

Bonjour,

Si l'implémentation semble correcte, la preuve est impossible car certains invariants sont faux, notamment:

((p_write>=p_read)=>(p_read..p_write-1)<|arr_vrb=pile) &
((p_write<p_read & p_write=1)=>(((p_read..MAX_ARR)<|arr_vrb))=pile) &
((p_write<p_read & p_write/=1)=>(((p_read..MAX_ARR)<|arr_vrb) \/ ((1..p_write-1)<|arr_vrb))=pile)

La séquence pile s'écrit {1 |-> pile(1), 2, |-> pile(2), ..., size(pile) |-> pile(size(pile)) }
Donc lorsque vous écrivez que pile = A <| arr_vrb (avec A une expression ensembliste), cette propriété n'est vraie que si A = 1..size(s) et si arr_vrb correspond très exactement à pile pour ces valeurs.
Or il suffit de dépiler une seule valeur (opération de lecture) pour décaler le début de A.

Une manière de traiter le problème est de spécifier une bijection bij telle que bij ; arr_vrb = pile
bij est dans ce cas un simple décalage si p_write n'a pas atteint MAX_ARR. Le calcul est un peu plus compliqué dans le cas contraire. bij est initialisée avec id.

[Laurent Guillaume]

Bonjour M. Lecomte,

Merci pour votre réponse mais je n'ai pas tout compris notamment
comment est définie la bijection bij de quoi vers quoi (A ? >-->> B ?)
comment est-elle initialisée et comment l'utiliser dans les opérations
de lecture et d'écriture ?

Bien à vous,

Laurent Guillaume

[Laurent Guillaume]

Bonjour,

J'ai finalement trouvé un modèle de FIFO que j'ai pu prouvé.
Il est inspiré de Okasaki.
L'idée est de raffiner la FIFO abstraite à l'aide d'une LIFO rear et front.
On pousse les éléments dans la Rear et on les dépile de la Front.
La Front contient l'inverse de la Rear.
A chaque fois que Front est vide et qu'on dépile, on la rempli avec
le contenu de la Rear que l'on vide , tous les éléments se retrouvent alors
dans la Front dans le bon ordre.

Soit ma FIFO BRing : seq(NAT) de taille max MaxFifoSize

PUT(vv) : BRing = vv->BRing
et
vv<-GET :
vv := last(BRing)
BRing := front(BRing)
J'ai omis les préconditions elles sont évidentes.
On raffine:

Front : seq(NAT)&
Rear : seq(NAT)

L'invariant devient:

BRing = rev(Rear)^Front (l'inverse de Rear concatené avec Front)
size(BRing) = size(Front) + size(Rear)

PUT(vv):
PRE size(Front) + size(Rear) < MaxFifoSize
Rear := Rear<-vv (car vv->BRing = rev(Rear<-vv)^Front)

vv <-- GET:
PRE size(Front) + size(Rear) > 0
IF Front=[] Front est vide donc on y copie rev(Rear) moins le dernier élément dépilé
Front=front(rev(Rear))
Rear=[] Rear est vidé
vv := last(rev(Rear)) le dernier élément dépilé est retourné
ELSE
Front:=front(Front) on dépile simplement
vv := last(Front

Ceci est plus facilement prouvé avec les règles disponibles.

Pour l'implémention il suffira de mapper deux tableaux sur Front et Rear

AFront : (0..MaxFifoSize) --> NAT
ARear : (0..MaxFifoSize) --> NAT

On sacrifie le premier élément (n° 0) pour être compatible avec le traducteur C qui ne supporte pas
directement les séquences dons l'index commence à 1 :

(1..MaxFifoSize)<|AFront = Front
(1..MaxFifoSize)<|ARear = Rear

On aura les index de chaque tableau :
FrontIdx = size(Front)
RearIdx = size(Rear)

Donc on n' a plus à prouver des expressions avec des index "modulo" tournant.
Mais on utilise 2x plus de mémoire et on fait une copie quand la Front est vide.

Cordialement.