Formale Spezifikation und Verifikation

anonymous@undisclosed.example.com (Anonymous) — Wed, 18 Nov 2020 17:11:25 +0000

2014-07-27 19:10		current
Line 284:		Line 284:

	* $RD_{{\color{ForestGreen}entry}}(\ell) = \bigcup_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}RD_{exit}({\color{red}\ell'})$		* $RD_{{\color{ForestGreen}entry}}(\ell) = \bigcup_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}RD_{exit}({\color{red}\ell'})$
-	* $RD_{exit}(\ell) = (RD_{entry}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$	+	* $RD_{exit}(\ell) = (RD_{{\color{ForestGreen}entry}}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$
	* Zu beginn werden //alle// Variablen mit "$(X, \ell)$" initialisiert.		* Zu beginn werden //alle// Variablen mit "$(X, \ell)$" initialisiert.

Line 291:		Line 291:
	"Verfügbare Ausdrücke" (Available Expressions)		"Verfügbare Ausdrücke" (Available Expressions)
	* $AE_{{\color{ForestGreen}entry}}(\ell) = {\color{blue}\bigcap}_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$		* $AE_{{\color{ForestGreen}entry}}(\ell) = {\color{blue}\bigcap}_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$
-	* $AE_{exit}(\ell) = (AE_{entry}(\ell) \setminus kill_{AE}(B^\ell)) \cup gen_{AE}(B^\ell)$	+	* $AE_{exit}(\ell) = (AE_{{\color{ForestGreen}entry}}(\ell) \setminus kill_{AE}(B^\ell)) \cup gen_{AE}(B^\ell)$
	* $kill_{AE}([x:=a]^\ell) = \{\text{Formeln, die }x\text{ enthalten}\}$		* $kill_{AE}([x:=a]^\ell) = \{\text{Formeln, die }x\text{ enthalten}\}$
	* $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ ohne }x\}$		* $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ ohne }x\}$

Wiki - uni:6:fsv

Formale Spezifikation und Verifikation