Développement des systèmes informatiques

Méthode de traces

Qu’est-ce qu’une trace ?

L’histoire d’exécution d’un module dès sa création.
Tous les événements qui influencent le module
Habituellement des invocations de programmes d’accès
Une sous-trace est une partie d’une trace, pas nécessairement sa partie initiale
Les assertions concernent des traces et pas de sous-traces

Pourquoi les traces sont-elles importantes ?

Chaque propriété du module qui concerne l’usager est visible.
Chaque propriété visible peut être exprimée en termes de traces et valeurs retournées.
Si nous pouvons définir l’ensemble de traces permises nous venons de définir les circonstances dans lesquelles le module doit fonctionner.
Si nous définissons des valeurs retournées en fonction de l’histoire (trace) nous venons de spécifier ce que le module doit faire.

Quand est-ce que deux traces sont équivalentes ?

Des traces équivalentes doivent être non-distinguables de l’extérieur du module.
Deux traces ne sont pas équivalentes si on ne peut pas montrer qu’elles sont équivalentes.

Qu’est-ce qu’une trace canonique ?

Le module étant un automate à états finis il y a des traces équivalentes.
La relation d’équivalence détermine un ensemble de classes d’équivalence.
Nous prenons un représentant de chaque classe qui sera traité comme trace canonique.

Exemple

Module pile avec les fonctions : PUSH(int I), POP(), TOP()

Exemple

Module int avec les fonctions : succ(), pred()

Pourquoi les traces canoniques sont-elles importantes ?

Elles fournissent une façon simple pour définir la relation d’équivalence.
Nous pouvons simplifier la description de certaines fonctions en restreignant le domaine à des traces canoniques.

Extensions d’une trace canonique par un événement

Le résultat peut être une trace canonique.
Le résultat peut être équivalent à une trace canonique.
Le dernier événement peut être illégal.

Il n’y a pas d’autres possibilités !

La fonction d'extension

Soit ext_P fonction d’extension pour le programme P

ext_P : traces canoniques x appels de P → traces canoniques

Exemple :

ext_PUSH(PUSH(2).PUSH(5), PUSH(3)) = PUSH(2).PUSH(5).PUSH(3)

PUSH(2).PUSH(5) représente l'état "avant", PUSH(3) représente un appel de PUSH (une extension de l'état "avant") et PUSH(2).PUSH(5).PUSH(3) représente le nouvel état.

Comment calculer la trace canonique équivalente à une trace donnée ?

Considérons la trace T égale à P₁(...).P₂(...). ... . P_n(...)

La trace canonique équivalente à T est définie à l’aide de la fonction red (réduction).

red(T) = extP_n( red(P₁(…).P₂(…). … . P_n-1(…) ), P_n(…)) si n > 1

red(T) = extP₁( _ , P₁(…)) si la trace vide est canonique

red(T) = extP₁( __c , P₁(…)) si la trace vide n’est pas canonique et _{_c} représente la trace canonique équivalente à la trace vide

Légalité

Trois catégories de jetons :

%legal% (le nouvel état de l'objet est défini par la fonction d'extension)
%fatal% (le nouvel état n'est pas défini)
%texte_différent_de_legal_et_fatal% (pas de changement d'état)

La légalité est définie pour les appels.

PUSH(4).POP().POP().PUSH(2).TOP().PUSH(6)

Le deuxième appel de POP() est illégal mais la trace entière est équivalente à PUSH(2).PUSH(6).

Notation

Ci-dessous x et y sont des noms d’objet, T, T1, T2 sont des traces et S est une portion d’une trace (une sous-chaîne de caractères).

symbolisme formel	signification
_ (soulignement)	trace vide
.	séparateur entre des éléments dans une représentation écrite de traces
[S]i=m..n	portion Z d’une trace qui est obtenue comme suit : dénotons par S_α la chaîne S dans laquelle toutes les occurrences de i ont été remplacées par α; Z = _ si m > n ou Z = S_m.S_m+1. ... .S_n si m ≤ n
(x,T1) ≡ (y,T2)	équivalence de traces (définie par la fonction d’extension)
T1 ≡ T2	∀ x,y; (x,T1) ≡ (y,T2)
*	symbole générique utilisé dans des traces canoniques
P(...)↓	la valeur retournée par l’invocation P(...)
P(..., a↓, ...)	la valeur retournée dans l’argument de sortie a
P(...)↓v	v est la valeur retournée par l’invocation P(...)
P(..., a↓b, ...)	b est la valeur retournée dans l’argument de sortie a
<M>	l'ensemble des traces canoniques dans le module M
<<M>>	l'ensemble de toutes les traces dans le module M

Exemples de traces

PUSH(a)
PUSH(a).Y(4)
_
[TOP.PUSH(a_i)]i=1..n
[PUSH(i).PUSH(a_i)]i=1..3
est équivalent à
PUSH(1).PUSH(a₁). PUSH(2).PUSH(a₂). PUSH(3).PUSH(a₃)
[PUSH(I).PUSH(a_i)]i=3..1
est équivalent à
_ (la trace vide)

Si une trace contient des appels de programmes non-déterministes, des valeurs de sortie apparaîtront dans cette trace.

Quelles informations trouverons-nous dans une spécification de module ?

Exemple

Nom de programme	Arg#1	Arg#2	Type de résultat
P	m:VO	int:V
Q	m:O
R	m:V		int

Remarque :

Les lettres V et O après le type d'argument (m ou int) décrivent le mode de passage d'argument :

V - argument d'entrée
O - argument de sortie
VO - argument d'entrée/sortie

Nous devons spécifier

la légalité de chaque appel
le nouvel état du premier argument de P
le nouvel état du premier argument de Q
la valeur retournée par R

Plus formellement, une spécification d’un module contient :

Une section syntaxique précisant les noms des programmes d’accès, les types d'arguments et le type de valeurs retournées
Un prédicat définissant la forme canonique des traces
Un ensemble de fonctions, une pour chaque programme, spécifiant la trace canonique équivalente à une extension d’une trace canonique par une invocation de ce programme
Ces fonctions définissent aussi la légalité de l’extension; l’image est (nouvelle trace, %classe%)
Un ensemble de relations/fonctions définissant l’ensemble de valeurs admissibles à retourner pour une trace canonique donnée

Propriétés de spécifications

Quand une spécification est-elle complète ?

le domaine de chaque fonction d’extension inclut toutes les traces canoniques
le domaine des relations définissant des valeurs inclut toutes les traces canoniques

Quand une spécification est-elle consistante ?

toutes les traces équivalentes doivent avoir le même ensemble de valeurs admissibles
les fonctions d’extension doivent être des fonctions

Comment traitons-nous le non-déterminisme ?

Dans des situations non-déterministes les valeurs peuvent être incluses dans la trace.
Mais des fonctions d’extension restent des fonctions!
Des fonctions définissant des valeurs retournées peuvent devenir des relations.

Objets nommés

Modules à objets multiples ont besoin d’un moyen pour nommer des objets.
Tous les deux (objets et noms) peuvent apparaître dans des traces.
Exemple :
CREATESTACK(n).PUSH(n, 5)

Symbole générique ("wild-card character") '*'

Les traces
CREATESTACK(n).PUSH(n, 5).PUSH(n,3)
et
CREATESTACK(m).PUSH(m, 5).PUSH(m,3)
doivent être traitées comme la même valeur.
Cette valeur est représentée par
CREATESTACK(*).PUSH(*, 5).PUSH(*,3)

Fonction d'extension (complément)

Comment interpréter la notation suivante ?
PUSH((n,T)↓, a) = T.PUSH(*,a)

Un état du module dont les objets sont dénotés par les noms n₁,n₂,...,n_n peut être présenté par une séquence
(n₁,val₁), (n₂,val₂), ..., (n_n,val_n)

L’effet de l’invocation PUSH(n,a) peut être illustré comme suit :
fonction d'extension

Exemples de spécifications

Spécification de l’interface du module Pile

(1) SYNTAXE

PROGRAMMES D'ACCÈS

Nom de programme	Arg#1	Arg#2	Type de résultat
PUSH	pile:VO	int:V
POP	pile:VO
TOP	pile:V		int

(2) TRACES CANONIQUES

canonique(T) ≡ ∃n:int, a₁,...,a_n:int; T = [PUSH(*, a_i)]i=1..n

(3) ÉQUIVALENCES

légalité(PUSH((n,T), a)) = %legal%

PUSH((n,T)↓, a) = T.PUSH(*, a)

légalité(POP((n,T))) =

Condition	Valeur
T = _	%vide%
T ≠ _	%legal%

POP((n,T)↓) = T1 where T1:<pile>; a:int; (T = T1.PUSH(*,a))

légalité(TOP(T)) =

Condition	Valeur
T = _	%vide%
T ≠ _	%legal%

TOP(T)↓ = a where T1:<pile>; a:int; (T = T1.PUSH(*, a))

Exercice : réduisez la trace ci-dessous à une trace canonique.

PUSH(n,5).POP(n).TOP(n).PUSH(n,3).PUSH(n,5).PUSH(n,11).POP(n).PUSH(n,7).POP(n)

Une autre spécification de l’interface du module Pile

(1) SYNTAXE

PROGRAMMES D'ACCÈS

Nom de programme	Arg#1	Arg#2	Type de résultat
CREATESTACK	pile:O
PUSH	pile:VO	int:V
POP	pile:VO
TOP	pile:V		int

(2) TRACES CANONIQUES

canonique(T) ≡ T = _ ∨ ∃n:int, a₁,...,a_n:int; T = CREATESTACK(*).[PUSH(*, a_i)]i=1..n

(3) ÉQUIVALENCES

légalité(CREATESTACK(n)) = %legal%

CREATESTACK(n↓) = CREATESTACK(*)

légalité(PUSH((n,T), a)) =

Condition	Valeur
T = _	%pile_invalide%
T ≠ _	%legal%

PUSH((n,T)↓, a) = T.PUSH(*, a)

légalité(POP((n,T))) =

Condition	Valeur
T = _	%pile_invalide%
length(T) = 1	%vide%
length(T) > 1	%legal%

POP((n,T)↓) = T1 where T1:<pile>; a:int; (T = T1.PUSH(*,a))

légalité(TOP(T)) =

Condition	Valeur
T = _	%pile_invalide%
length(T) = 1	%vide%
length(T) > 1	%legal%

TOP(T)↓ = a where T1:<pile>; a:int; (T = T1.PUSH(*, a))

Spécification de l’interface du module File12

Introduction informelle

Le module implémente une file d’entiers dont la capacité ≤ 12.

(1) SYNTAXE

PROGRAMMES D'ACCÈS

Nom de programme	Arg#1	Arg#2	Type de résultat
ADD	file12:VO	int:V
REMOVE	file12:VO
FRONT	file12:V		int

(2) TRACES CANONIQUES

canonique(T) ≡ ∃n:int, a₁,...,a_n:int; (T = [ADD(*, a_i)]i=1..n ∧ 0 ≤ n ≤ 12)

(3) ÉQUIVALENCES

légalité(ADD((n,T), a)) =

Condition	Valeur
length(T) = 12	%pleine%
length(T) < 12	%legal%

ADD((n,T)↓, a) = T.ADD(*, a)

légalité(REMOVE((n,T))) =

Condition	Valeur
T = _	%vide%
T ≠ _	%legal%

REMOVE((n,T)↓) = T1 where T1:<file12>; a:int; (T = ADD(*,a).T1)

légalité(FRONT(T)) =

Condition	Valeur
T = _	%vide%
T ≠ _	%legal%

FRONT(T)↓ = a where T1:<file12>; a:int; (T = ADD(*, a).T1)

Spécification de l’interface du module Pile(taille)

(1) SYNTAXE

PROGRAMMES D'ACCÈS

Nom de programme	Arg#1	Arg#2	Type de résultat
PUSH	pile:VO	int:V
POP	pile:VO
TOP	pile:V		int

(2) TRACES CANONIQUES

canonique(T) ≡ ∃n:int, a₁,...,a_n:int; (T = [PUSH(*, a_i)]i=1..n ∧ n ≤ taille)

(3) ÉQUIVALENCES

légalité(PUSH((n,T), a)) = %legal%

PUSH((n,T)↓, a) =

Condition	Valeur
length(T) < taille	T.PUSH(*, a)
length(T) = taille	T1.PUSH(, a) where T1:<pile> b:int; (T = PUSH(, b).T1)

légalité(POP((n,T))) =

Condition	Valeur
T = _	%vide%
T ≠ _	%legal%

POP((n,T)↓) = T1 where T1:<pile>; a:int; (T = T1.PUSH(*,a))

légalité(TOP(T)) =

Condition	Valeur
T = _	%vide%
T ≠ _	%legal%

TOP(T)↓ = a mod 255 where T1:<pile>; a:int; (T = T1.PUSH(*, a))

Spécification de l’interface du module Producteur d'entiers

(0) Caractéristiques

type specifié: intg

(1) SYNTAXE

PROGRAMMES D'ACCÈS

Nom de programme	Arg#1	Type de résultat
GETINT	intg:VO	int:R

Commentaire : 'R' est utilisé pour indiquer une valeur non-déterministe.

(2) TRACES CANONIQUES

canonique(T) ≡ ∃n:int, x₁,...,x_n:int; (T = [GETINT(*)↓x_i)]i=1..n ∧ ∀i:int; (1 ≤ i ≤ n ⇒ x_i < x_i+1))

(3) ÉQUIVALENCES

légalité(GETINT((n,T))) = %legal%

GETINT((n,T)↓)↓v = S1.GETINT(*)↓v.S2 where S1,S2:<intg> (T = S1.S2 ∧ canonique(S1.GETINT(*)↓v.S2))

GETINT((n,T))↓a | ¬∃S1,S2:<intg> [T = S1.GETINT(*)↓a.S2]

Traces utilisées comme valeurs

Nous avons besoin d’une notation pour des valeurs littérales de types abstraits.
Les traces canoniques peuvent jouer ce rôle.
Des abréviations peuvent être définies en termes de traces canoniques.
Ces valeurs peuvent être utilisées dans notre sémantique relationnelle de programmes.