Wiki

A universe of ideas

User Tools

Site Tools

You are here: A universe of ideas » Uni » 6. Semester » Formale Spezifikation und Verifikation
Trace:
uni:6:fsv:start

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
uni:6:fsv:start [2014-07-20 00:27] – [Datenflussgleichung] skrupellosuni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
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_{exit}(\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_{exit}(\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{ und }x \not\in a\}$ +  * $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ ohne }x\}$ 
-  * $gen_{AE}([bool exp]) = \{\text{Teilausdrücke von }bool exp\}$+  * $gen_{AE}([bool\ exp]) = \{\text{Teilausdrücke von }bool\ exp\}$
   * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.   * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.
   * //Nur// Arithmetische Ausdrücke   * //Nur// Arithmetische Ausdrücke
Line 303: Line 303:
   * $LV_{{\color{ForestGreen}entry}}(\ell) = (LV_{exit}(\ell) \setminus kill_{LV}(B^\ell)) \cup gen_{LV}(B^\ell)$   * $LV_{{\color{ForestGreen}entry}}(\ell) = (LV_{exit}(\ell) \setminus kill_{LV}(B^\ell)) \cup gen_{LV}(B^\ell)$
   * $kill_{LV}([x:=a]^\ell) = \{x\}$   * $kill_{LV}([x:=a]^\ell) = \{x\}$
-  * $gen_{LV}([x := a]) = \{\text{Teilausdrücke von }a\}$ +  * $gen_{LV}([x := a]) = \{\text{Variablen in }a\}$ 
-  * $gen_{LV}([bool exp]) = \{\text{Teilausdrücke von }bool exp\}$+  * $gen_{LV}([bool\ exp]) = \{\text{Variablen in }bool\ exp\}$
   * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.   * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.
  
Line 416: Line 416:
 </code> </code>
  
 +===== Beweise =====
 +==== Vollständiger Verband ====
 +Verband $(L, \sqsubseteq)$
 +  * **reflexiv** \\ $\forall_{x \in L} : x \sqsubseteq x$
 +  * **transitiv** \\ $\forall_{x, y, z \in L} : x \sqsubseteq y \wedge y \sqsubseteq z \Rightarrow x \sqsubseteq z$
 +  * **antisymetrisch** \\ $\forall_{x, y \in L} : x \sqsubseteq y \wedge y \sqsubseteq x \Rightarrow x = y$
 +  * **Jede Teilmenge hat ein Supremum** \\ Jedes $U \subseteq L$ hat ein $\bigsqcup U$
 +
 +==== Supremum ====
 +$s = \bigsqcup U$
 +
 +  * **Ist obere Schranke** \\ $\forall_{x \in U} : x \sqsubseteq s$
 +  * **Ist //kleinste// obere Schranke** \\ $s' \text{ ist obere Schranke } \Rightarrow s \sqsubseteq s'$
 +
 +==== Monotonie ====
 +  * $x \sqsubseteq y \Rightarrow F(x) \sqsubseteq F(y)$
 + 
 +==== Fixpunkt ====
 +  * $\exists x: F(x) = x$
 +
 +Dazu muss $F(x)$ monoton sein.
 ===== Probleme ===== ===== Probleme =====
 ==== Semaphor ==== ==== Semaphor ====
uni/6/fsv/start.1405808859.txt.gz · Last modified: (external edit)