###### 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$