---
# System prepended metadata

title: Modellierung
tags: [FS3]

---

###### tags: `FS3`
# Modellierung
## Endliche Folgen
## Relationen
- Relation $R \subseteq M_1 \times ... \times M_n$
    - z.B. $SPRACHKOMPETENZ \subseteq DEL \times SPRACHE$. Das Tupel $(v,s)$ ist Teil der Relation, wenn Deligierter $v$ die Sprache $s$ spricht
- Notation: $R(s_1,...,s_n)$
- Können verwendet werden, um Anforderungen an Funktionen zu definieren: $f \in ANFORDERUNG \Leftrightarrow \psi_1$, wobei $ANFORDERUNG$ eine Relation mit über die selben Mengen wie $f$ ist
## Funktionen
- totale Funktion: jedes $d \in D$ hat ein $b \in B$, so dass $(d,b) \in f$
- falls es zu $d$ kein $b$ gibt, schreibt man $f(d)↑$
- Definition: 
    - $f: D → B$
    - $f(x):= 
        \begin{cases} 
        a,\:\:\:   if\:\: condition 1 \\
        b,\:\:\:   if\:\: condition 2 \\
        c,\:\:\:   else
        \end{cases}$
- Funktionen können auch Mengen zurückgeben 
    - $f: D → P(B)$
    - $f(x):= \{b \in B|(x,b)\in R\}$ wobei $R \subseteq D \times B$ eine Relation
## Indexmengen
- $INDEX:= \{1,2,3\}$
- $DEL:=NATION \times INDEX$
## Kardinalität
- Für Mengen: Anzahl ihrer Elemente $|M|$
- Für Potenzmenge: $|P(M)|=2^{|M|}$
- Für Funktionen: $|D→B|=(|B|+1)^{|D|}$
## Prädikate
- Prädikat über Menge $M$ ist eine Funktion $p: M→\mathbb{B}$ mit $\mathbb{B}:=\{\mathfrak{w,f}\}$

# Logik
## Syntax Der Aussagenlogik

### Junktoren:

- Negation ("nicht A"): $\neg A$
- Disjunktion ("A oder B"): $A \vee B$
- Konjunktion ("A und B"): $A \wedge B := \neg (\neg A \vee \neg B)$
- Implikation ("wenn A, dann B"): $A \Rightarrow B := (\neg A) \vee B$
- Bi-Implikation ("A genau dann, wenn B"): $A \Leftrightarrow B := (A \wedge B) \vee (\neg A \wedge \neg B)$

## Semantik der  Aussagenlogik

### Belegung von Formeln

- Eine Belegung $\mathfrak{I}$ ist eine totale Funktion $\cdot ^ \mathfrak{I}: AL(V) \rightarrow \{\mathfrak{w}, \mathfrak{f}\}$
> Eine Belegung bildet alle Variablensymbole auf Wahrheitswerte ab.

### Modellbeziehung

- $\mathfrak{I}$ ist ein Modell von $\alpha \in AL(V)$ wenn $\alpha ^ \mathfrak{I} = \mathfrak{w}$
- $\mathfrak{I}$ ist ein Modell von $\phi \in AL(V)$ wenn $\phi ^ \mathfrak{I} = \mathfrak{w}$
> Eine Belegung ist ein Modell wenn eine Formel/Formelmenge für diese Belegung wahr wird.

### Erfüllbarkeit

- $\alpha$ ist erfüllbar genau dann, wenn $\mathfrak{I} \models \alpha$ für mindestens eine Belegung $\mathfrak{I}$ gilt.
- $\phi$ ist erfüllbar genau dann, wenn $\mathfrak{I} \models \phi$ für mindestens eine Belegung $\mathfrak{I}$ gilt.
> Eine Formel/Formelmenge ist erfüllbar genau dann, wenn sie ein Modell hat.

### Allgemeingültigkeit

- $\alpha$ ist allgemeingültig genau dann, wenn $\mathfrak{I} \models \alpha$ für alle Belegungen $\mathfrak{I}$ gilt.
- $\phi$ ist allgemeingültig genau dann, wenn $\mathfrak{I} \models \phi$ für alle Belegungen $\mathfrak{I}$ gilt.
> Eine Formel/Formelmenge ist allgemeingültig genau dann, wenn jede Belegung ein Modell der Funktion ist.
- $\models \beta$ genau dann, wenn $\beta$ allgemeingültig.

### Semantische Folgerung

- Seien $\phi \subseteq AL(V)$ und $\alpha \in AL(V)$. Gilt für jede Belegung $\mathfrak{I}$, für die $\mathfrak{I} \models \phi$ gilt, auch $\mathfrak{I} \models \alpha$ gilt, dann gilt $\phi \models \alpha$.
> Eine Formelmenge $\phi$ modelliert eine Formel $\alpha$ wenn jede Belegung die $\phi$ modelliert auch $\alpha$ modelliert.
- $\alpha \models \beta$ genau dann, wenn $\alpha \Rightarrow \beta$ allgemeingültig.

### semantische Äquivalenz

- Sei $\alpha , \beta \in AL(V)$. $\alpha$ und $\beta$ sind semantisch äquivalent, genau dann, wenn für alle Belegungen $\mathfrak{I}$ gilt: $\alpha ^ \mathfrak{I} = \beta ^ \mathfrak{I}$ und wir schreiben $\alpha \approx \beta$.
> Zwei Formelmengen sind semantisch equivalent wenn sie für alle Belegungen die selbe Bedeutung haben.
-  $\alpha \approx \beta$ genau dann, wenn $\alpha ^ \mathfrak{I} = \beta ^ \mathfrak{I}$ und $\alpha \Leftrightarrow \beta$ gilt.

## Endlichkeitssatz der Aussagenlogik

- Die Formelmenge $\phi$ ist genau dann erfüllbar, wenn jede endliche Teilmenge $\phi_0 \subseteq \phi$ erfüllbar ist.
- $\phi \models \psi$ gilt genau dann, wenn für eine endliche Teilmenge $\phi_0 \subseteq \phi$ gilt: $\phi_0 \models \psi$
> Eine Formelmenge $\phi$ modelliert eine Formel $\psi$ wenn eine Teilmenge von $\phi$, $\psi$ modelliert.

## Normalformen

- KNF: $( A \vee B ) \wedge ( C \vee D )$
- KNF: $( A \wedge B ) \vee ( C \wedge D )$

# Spezifikation

## Regex
- $\emptyset \in REG(\sum)$
- $a \in REG(\sum)$
- $(a+b) \in REG(\sum)$ wenn $a,b \in REG(\sum)$
- $(ab) \in REG(\sum)$ wenn $a,b \in REG(\sum)$
- $(a^*) \in REG(\sum)$ wenn $a \in REG(\sum)$

## Grammatiken

- $G = (\Sigma, V, X_0, P)$
	- $\Sigma$: Das Alphabet der Grammatik
	- $V$: Die Variablen der Grammatik $( \Sigma \cap V = \emptyset )$
	- $X_0$: Startsymbol $( X_0 \in V )$
	- $P$: Produktionsregeln $(P \subseteq (\Sigma \cup V)^+ \times (\Sigma \cup V)^*)$

## Backus Naur Form

- Beispiel $G = \{\{\langle, \rangle, \vee, -, v\}, \{A, B\}, A, \{A \rightarrow \langle B \rangle, A \rightarrow v, B \rightarrow A \vee A, B \rightarrow \neg A\}\}$
- BNF:
	- $A ::= \langle B \rangle \mid v$
	- $B ::= A \vee A \mid \neg A$

# Programmiersprachen

## Semantik für AExp

$$r\oplus \frac
{
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow n_1
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow n_2
	\end{align*}
}
{
	\langle
		( a_1 \oplus a_2 ), \sigma
	\rangle
	\Downarrow n
}
n \text{ ist die Summe von } n_1 \text{ und } n_2$$

$$r\ominus \frac
{
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow n_1
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow n_2
	\end{align*}
}
{
	\langle
		( a_1 \ominus a_2 ), \sigma
	\rangle
	\Downarrow n
}
n \text{ ist die Differenz von } n_1 \text{ und } n_2$$

$$r\odot \frac
{
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow n_1
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow n_2
	\end{align*}
}
{
	\langle
		( a_1 \odot a_2 ), \sigma
	\rangle
	\Downarrow n
}
n \text{ ist das Produkt von } n_1 \text{ und } n_2$$

$$rVar \frac
{
}
{
	\langle
		X, \sigma
	\rangle
	\Downarrow n
}
n = \sigma(X)$$

$$rNum \frac
{
}
{
	\langle
		n, \sigma
	\rangle
	\Downarrow n
}$$

## Semantik für BExp

$$\text{rt} \frac
{
}
{
	\langle
		true, \sigma
	\rangle
	\Downarrow true
}$$

$$\text{rf} \frac
{
}
{
	\langle
		false, \sigma
	\rangle
	\Downarrow false
}$$

### Gleich

$$\text{reqt} \frac {
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow n_1
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow n_2
	\end{align*}
} {
	\langle
		( a_1 \: eq \: a_2), \sigma
	\rangle
	\Downarrow true
}
n_1 = n_2$$

$$\text{reqf} \frac {
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow n_1
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow n_2
	\end{align*}
} {
	\langle
		( a_1 \: eq \: a_2), \sigma
	\rangle
	\Downarrow false
}
n_1 \neq n_2$$

### Kleiner Gleich

$$\text{rleqt} \frac {
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow n_1
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow n_2
	\end{align*}
} {
	\langle
		( a_1 \: leq \: a_2), \sigma
	\rangle
	\Downarrow true
}
n_1 \leq n_2$$

$$\text{rleqf} \frac {
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow n_1
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow n_2
	\end{align*}
} {
	\langle
		( a_1 \: leq \: a_2), \sigma
	\rangle
	\Downarrow false
}
n_1 > n_2$$

### Nicht

$$\begin{align}
    \text{rnott} \frac {
        \langle
            a, \sigma
        \rangle
        \Downarrow false
    } {
	    \langle
		    not \: a, \sigma
	    \rangle
	    \Downarrow true
    }
&&
    \text{rnotf} \frac {
        \langle
            a, \sigma
        \rangle
        \Downarrow true
    } {
	    \langle
		    not \: a, \sigma
	    \rangle
	    \Downarrow false
    }
\end{align}$$

### Und

$$\text{randt} \frac {
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow true
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow true
	\end{align*}
} {
	\langle
		( a_1 \: and \: a_2), \sigma
	\rangle
	\Downarrow true
}$$

$$\begin{align*}
        randf1 \frac {
        \langle
            a_1, \sigma
        \rangle
        \Downarrow false
    } {
	    \langle
		    ( a_1 \: and \: a_2), \sigma
	    \rangle
	    \Downarrow false
    }
&&
    randf2 \frac {
        \langle
            a_2, \sigma
        \rangle
        \Downarrow false
    } {
	    \langle
		    ( a_1 \: and \: a_2), \sigma
	    \rangle
	    \Downarrow false
    }
\end{align*}$$

### Oder

$$\begin{align*}
        rort1 \frac {
        \langle
            a_1, \sigma
        \rangle
        \Downarrow true
    } {
	    \langle
		    ( a_1 \: or \: a_2), \sigma
	    \rangle
	    \Downarrow true
    }
&&
    rort2 \frac {
        \langle
            a_2, \sigma
        \rangle
        \Downarrow true
    } {
	    \langle
		    ( a_1 \: or \: a_2), \sigma
	    \rangle
	    \Downarrow true
    }
\end{align*}$$

$$rorf \frac {
	\begin{align*}
		\langle
			a_1, \sigma
		\rangle
		\Downarrow false
		&&
		\langle
			a_2, \sigma
		\rangle
		\Downarrow false
	\end{align*}
} {
	\langle
		( a_1 \: or \: a_2), \sigma
	\rangle
	\Downarrow false
}$$

## Com

$$rsk \frac {
} {
	\langle
		skip, \sigma
	\rangle
	\rightarrow \sigma
}$$

$$r: \frac {
    \langle
		a, \sigma
	\rangle
	\Downarrow n
} {
	\langle
		X := a, \sigma
	\rangle
	\rightarrow \sigma'
}$$

$$r; \frac {
    \begin{align*}
		\langle
		    c_1, \sigma
	    \rangle
	    \rightarrow \sigma''
		&&
		\langle
		    c_2, \sigma''
	    \rangle
	    \rightarrow \sigma'
	\end{align*}
} {
	\langle
		c_1;c_2, \sigma
	\rangle
	\rightarrow \sigma'
}$$

$$rift \frac {
    \begin{align*}
		\langle
		    b, \sigma
	    \rangle
	    \Downarrow true
		&&
		\langle
		    c_1, \sigma
	    \rangle
	    \rightarrow \sigma'
	\end{align*}
} {
	\langle
		if \: b \: then \: c_1 \: else \: c_2, \sigma
	\rangle
	\rightarrow \sigma'
}$$

$$riff \frac {
    \begin{align*}
		\langle
		    b, \sigma
	    \rangle
	    \Downarrow false
		&&
		\langle
		    c_2, \sigma
	    \rangle
	    \rightarrow \sigma'
	\end{align*}
} {
	\langle
		if \: b \: then \: c_1 \: else \: c_2, \sigma
	\rangle
	\rightarrow \sigma'
}$$

$$rwht \frac {
    \begin{align*}
		\langle
		    b, \sigma
	    \rangle
	    \Downarrow true
		&&
		\langle
		    c, \sigma
	    \rangle
	    \rightarrow \sigma''
        &&
		\langle
		    while \: b \: do \: c \: od , \sigma''
	    \rangle
	    \rightarrow \sigma'
	\end{align*}
} {
	\langle
		while \: b \: do \: c \: od, \sigma
	\rangle
	\rightarrow \sigma'
}$$

$$rwhf \frac {
    \langle
        b, \sigma
    \rangle
    \Downarrow false
} {
	\langle
		while \: b \: do \: c \: od, \sigma
	\rangle
	\rightarrow \sigma'
}$$

# Beweisansätze
## strukturelle Induktion
- "Prinzip der str. Induktion": 
    - P(false)
    - P(true)
    - $\to$