forked from petervanroy/lingi1101
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpartie14.tex
156 lines (136 loc) · 7.3 KB
/
partie14.tex
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
%\section*{Suite des exemples de la première heure}
\section{Théorie des ensembles}
Nous introduisons une version simple de la théorie des ensembles
comme prérequis pour la spécification des systèmes avec l'approche Z.
Informellement, il y a deux manières de définir des ensembles:
\begin{itemize}
\item Un ensemble peut être défini comme une énumération d'éléments, comme par exemple
\{0,20,40,60,80,100 \} ou \{Mercure, Vénus, Terre, ..., Neptune\}.
\item Un ensemble peut également être défini avec un prédicat d'un argument qui est vrai pour les membres.
On appelle cette définition une {\em compréhension}.
Certains langages de programmation (comme Python ou Haskell) possèdent des syntaxes particulières dédiées
à la création de listes remplies par des compréhensions.
Par exemple: \{ n | n $\in$ $\mathbb{N}$ $\wedge$ $\exists$ k, k $\in$ $\mathbb{N}$ $\wedge$ 20k = n $\wedge$ 0 $\leq$ n $\leq$ 100 \}.
\end{itemize}
Les axiomes vont en partie suivre cette intuition.
Nous introduisons maintenant les axiomes pour les ensembles.
\textbf{Axiomes}
\begin{itemize}
\item \textbf{Égalité} (première définition) \\
A = B $\Leftrightarrow$ ($\forall$ x) (x $\in$ A $\Leftrightarrow$ x $\in$ B)\\
\item \textbf{Ensemble vide} (sans éléments)\\
$\emptyset$ = \{\} = \{x $\vert$ x $\neq$ x\}\\
\item \textbf{Ensemble universel} (tous les éléments du domaine)\\
$\mathcal{U}$ (par exemple: $\mathbb{N}$, $\mathbb{R}$, $\mathbb{Z}$)\\
\item \textbf{Sous-ensemble}\\
A $\subseteq$ B $\Leftrightarrow$ ($\forall$ x) (x $\in$ A $\Rightarrow$ x $\in$ B)\\
A $\nsubseteq$ B $\Leftrightarrow$ $\neg$(A $\subseteq$ B)\\
A $\subset$ B $\Leftrightarrow$ A $\subseteq$ B $\wedge$ A $\neq$ B\\
\item \textbf{Construction de sous ensemble} \\
A $\subseteq$ B $\Leftrightarrow$ (x $\in$ A $\Leftrightarrow$ x $\in$ B $\wedge$ $\varphi$(x))\\
On va ici prendre des éléments de B tels que $\varphi$(x) est vrai, et les mettre dans A. C'est un peu une formulation de la notion de compréhension.\\
\item \textbf{Propriétés}\\
$\emptyset$ $\subseteq$ A\\
A $\subseteq$ A\\
A $\subseteq$ B $\wedge$ B $\subseteq$ C $\Rightarrow$ A $\subseteq$ C \\
\item \textbf{Égalité} (2e définition)\\
(A = B) $\Leftrightarrow$ (A $\subseteq$ B) $\wedge$ (B $\subseteq$ A)\\
\item \textbf{Taille d'un ensemble}
\begin{itemize}
\item Prédicat à 2 arguments\\
\#(A,n) : A contient n éléments\\
\#$\emptyset$ = 0 $\rightarrow$ \#($\emptyset$, 0)
\item $\mathbb{P}$A = \{a $\vert$ a $\subseteq$ A\} (prédicat à 2 arguments) : ensemble des sous-ensembles de A\\
\#$\mathbb{P}$A = 2$^{\#A}$ \\
\end{itemize}
\end{itemize}
\subsection{Spécification formelle avec l'approche Z}
L'approche Z utilise la logique des prédicat et est basée sur la théorie des ensembles.
C'est une approche ``orientée modèle''': on ne donne pas que les équations, mais aussi la structure du système.
Dans cette section nous donnons une introduction à l'approche Z avec un exemple simple
de gestion de stock dans une bibliothèque.
\subsubsection{Concepts en Z}
Type:\\
\begin{itemize}
\item Types génériques (ensembles): par exemple : Book, Location
\item Types énumérés: par exemple : \\
Status := $\underbrace{In}_{Dans \hspace{0.1cm} la \hspace{0.1cm} bibliothèque, \hspace{0.1cm} disponible}$ $\vert$ $\overbrace{Out}^{Prêté}$ $\vert$ $\underbrace{Ref}_{Livre \hspace{0.1cm} de \hspace{0.1cm} référence}$ \\
\end{itemize}
Schéma:\\
\begin{itemize}
\item Nom: le nom d'un composant du système
\item Signature: une énumération des variables utilisées avec leurs types, et une description de la transformation faite par le composant
\item Prédicat: des formules en logique des prédicats qui décrivent l'état du système
\item Comportement: voir suivant\\
\end{itemize}
Comportement:\\
\begin{itemize}
\item Précondition du système: formule en logique des prédicats, ce qui doit être vrai avant pour que le composant soit applicable
\item Postcondition du système: formule en logique des prédicats, ce qui est vrai après l'application du composant
\item Transformation de l'état: formule en logique des prédicats, équations entre état initial et terminal du composant
\end{itemize}
La définition d'un comportement utilise une sémantique et une syntaxe particulière pour décrire les transformtations d'état.
Une exécution est une séquence d'états et chaque application d'un composant avant l'exécution d'un pas avec
un avant et un après:
\begin{center}
\includegraphics[scale=0.5]{images/14_sequence.png}
\end{center}
Les variables avant sont écrites normalement (Lib\_Stock) et les variables après sont écrites avec un apostrophe
(Lib\_Stock').
Il y a une syntaxe particulière pour décrire ce qui se passe avec les états avant et après:
\begin{itemize}
\item $\Delta$ Lib\_Stock: état avant (Lib\_Stock) et après (Lib\_Stock')
\item $\Xi$ Lib\_Stock: état avant et après s'ils sont identiques
\end{itemize}
Les définitions de ces deux symboles sont:
\begin{itemize}
\item $\Delta$ Lib\_Stock $\triangleq$ Lib\_Stock $\wedge$ Lib\_Stock'
\item $\Xi$ Lib\_Stock $\triangleq$ Lib\_Stock $\wedge$ Lib\_Stock' $\mid$ Lib\_Stock=Lib\_Stock'
\end{itemize}
\subsubsection{Exemple d'un état}
\begin{center}
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
\begin{tabular}{|l|M{7cm}|}
\hline
nom & \hspace{2cm} LIB\_STOCK \tabularnewline
\hline
signature & stock\\ on\_loan\\ on\_shelf\\ ref\_coll : $\mathbb{F}$ Book \tabularnewline
\hline
prédicat & stock = on\_loan $\cup$ on\_shelf\\ on\_loan $\cap$ on\_shelf = $\emptyset$\\ ret\_call $\subseteq$ on\_shelf \tabularnewline
\hline
\end{tabular}
\end{center}
La notation $\mathbb{F}$ Book représente un sous-ensemble {\em fini} de l'ensemble Book.\\
\subsubsection{Exemple d'un comportement}
\begin{center}
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
\begin{tabular}{|l|M{7cm}|}
\hline
nom & \hspace{2cm} ADD\_STOCKo \tabularnewline
\hline
signature & $\Delta$ Lib\_Stock\\ new ? : $\mathbb{F}$ Book \tabularnewline
\hline
prédicat & new ? $\neq$ $\emptyset$ \hfill $\rightarrow$ précondition\\ new ? $\wedge$ stock = $\emptyset$ \hfill $\rightarrow$ précondition\\ stock' = stock $\cup$ new ? \hfill $\rightarrow$ postcondition\\ on\_loan' = on\_loan \hfill $\rightarrow$ postcondition\tabularnewline
\hline
\end{tabular}
\end{center}
Le "?" signifie qu'il s'agit d'une entrée.
On peut déduire de ces prédicats que new? sera dans on\_shelf.
Si la ou les préconditions ne sont pas satisfaites, on aura des erreurs que l'on devra corriger via la gestion d'erreurs.
Si les préconditions n'échouent jamais, on a affaire à une opération totale.
\subsubsection{Exemple d'opération totale}
On peut définir une operation totale en ajoutant un traitement d'erreur:
ADD\_STOCK = ADD\_STOCK${}_0$ $\cup$ ERRONEOUS\_NEW\_STOCK
\begin{center}
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
\begin{tabular}{|l|M{8.5cm}|}
\hline
nom & \hspace{1cm}ERRONEOUS\_NEW\_STOCK \tabularnewline
\hline
signature & $\Xi$ Lib\_Stock\\ new ? : \# Book\\ rep! : Report \tabularnewline
\hline
prédicat & (new ? = $\emptyset$ $\vee$ new ? $\cap$ stock $\neq$ $\emptyset$) \hfill $\rightarrow$ préconditions\\ rep ! = "Attention stock problem" \tabularnewline
\hline
\end{tabular}
\end{center}
Le "!" signifie qu'il s'agit d'une sortie.