Développement des systèmes informatiques

Conception interne du module File12

(1) Structure de données

Type	Noms de variables	Valeur initiale
int [12]	tab	"peu importe"
int	t, d	0, 1 ^(*)
boolean	plein	false

^(*) Toutes les valeurs qui satisfont "bord" pourraient être utilisées.

Dictionnaire

Symbole	Valeur
bord	(d = t + 1) ∨ (t = 11) ∧ (d = 0)
'bord	‘bord = (‘d = ‘t + 1) ∨ (‘t = 11) ∧ (‘d = 0)
ds	int[12] x int x int x boolean

(2) Fonction d'abstraction

af : ds → <File12>

af(tab, t, d, plein) =

Condition	Trace canonique
(¬ bord ∨ plein) ∧ (t ≥ d)	[ADD(*, tab[t-i])]i=0..t-d
(¬ bord ∨ plein) ∧ (t < d)	[ADD(, tab[t-i)]i=0..t . [ADD(, tab[11+d-i)]i=d..11
bord ∧ ¬plein	_

(3) Fonctions de programme

Nom de fonction de programme	Arg#1	Signature
pf_ADD	int	ds → ds
pf_REMOVE		ds → ds
pf_FRONT		ds → ds x int

pf_ADD = NC(t) ∧ ∀j:int; (0 ≤ j ≤ 11 ∧ j ≠ d' ⇒ NC(tab[j])) ∧

	('d = 0) ∧			('d ≠ 0) ∧
	'bord ∧		¬ 'bord	'bord ∧		¬ 'bord
	'plein	¬'plein	¬ 'bord	'plein	¬'plein	¬ 'bord
tab'[d'] =	'tab['d]	a	a	'tab['d]	a	a
d' =	'd	11	11	'd	'd - 1	'd - 1
plein' =	'plein	false	't = 10	'plein	false	true

pf_REMOVE = NC(tab, d) ∧

	(¬'bord ∨ 'plein) ∧		'bord ∧ ¬'plein
	('t = 0)	('t > 0)	'bord ∧ ¬'plein
t' =	11	't - 1	't
plein' =	false	false	'plein

pf_FRONT = NC(tab, t, d, plein) ∧ (return = 'tab['t])