# Formale Methoden im Softwareentwurf SoSe 2022

## Endliche Automaten
Definition: $M = (Q, R, s, F, \Sigma)$
- $Q$ = Zustandsmenge
- $R$ = Übergangsrelation $Q \times \Sigma \times Q$
- $s \in Q$ = Startzustand
- $F \subseteq Q$ Menge der Endzustände
- $\Sigma$ = Eingabealphabet

## Aussagelogik
Gültigkeit
- Eine Formel $\varphi$ ist gültig, wenn für alle Interpretationen $I$ gilt = $I \vDash \varphi$
- Wir schreiben dann: $\vDash \varphi$ (Tautologie)

Erfüllbarkeit
- Eine Formel $\varphi$ ist erfüllbar, wenn es eine Interpretation $I$ gibt mit $I \vDash \varphi$

Implikation:
- $a \rightarrow b = \neg a \lor b$

Äquivalenz
- $a \leftrightarrow b = (a \rightarrow b) \land (b \rightarrow a) = (\neg a \lor b) \land (\neg b \lor a)$

## Transitionssysteme
Definition: $TS = (S, Act, \rightarrow, I, AP, L)$
- $S$ = menge an Zuständen
- $Act$ = Menge an Aktionen
- $\rightarrow \subseteq S \times Act \times S$ = Transitionsrelation
- $s \xrightarrow{\alpha} s'$ = $(s, \alpha, s'$)
- $I$ = Menge an Anfangszuständen
- $AP$ = Menge an atomaren Propositionen (Aussagen, die wahr oder falsch sein können)
- $L: S \rightarrow 2^{AP}$ Beschriftungsfunktion, die jedem Zustand eine Menge von wahren atomaren Propositionen zuordnet

### Handschlag mit Handschlagsaktionsset H
- Wir betrachten hier die Menge $H$
- Wir schauen uns alle Transitionssysteme an und konstruieren das Produkt beider Transistionsysteme
- Neue Übergänge entsprechen Kombination aus alten Übergänge
- Beachte hierbei, dass wir nur die Übergänge betrachten, die das Alphabet in $H$ enthalten

$\Rightarrow$ Nebenläufige Prozesse können nur miteinander kommunizieren, wenn sie gleichzeitig eine Handschlagaktion der Menge $H$ ausführen

## Programmgraph
Definition: $PG = (Loc, Act, Effect, \hookrightarrow, Loc_0, g_0)$
- $Loc$ = Menge an Positionen (Zustände)
- $Act$ = Menge an Aktionen
- bspw. $\alpha$ mit $x := x + 1$
- $Effect = Act \times Eval(Var) \rightarrow Eval(Var)$ einer Effekt-Funktion
- $Var$ = Menge an typisierten Variablen
- Jede Variable $x \in Var$ ist ein Wertebereich $dom(x)$ zugeordnet bspw. boolean, integer, {rot, grün}, ...
- $Eval(Var)$ = Menge an Variablenbelegung bspw. $n \in Eval(Var)$ weist die folgenden Werte den Variablen $x, y$ zu
- $n(x)$ = true
- $n(y)$ = false
- $\hookrightarrow \subseteq Loc \times Cond(Var) \times Act \times Loc$ einer bedigten Transitionsrelation
- $l \xrightarrow{g:\alpha} l' = (l, g, \alpha, l')$
- $Loc_0 \subseteq Loc$ = Menge an Initialpositionen (Anfangszustände)
- $g_0 \in Cond(Var)$ = Initialbedingung

### PG in TS
- Zustände sind Tupel aus (Position, Variablenbelegung)
- Anfangszustände sind Kombinationen aus Initialpositionen und Variablenbelegungen, die $g_0$ erfüllen.
- Transitionen sind alle möglichen Übergänge aus PG. Beachte hierbei die Variablenbelegung

## Temporale Logik LTL
Zustandsquantoren:
- $X \dots$ "im nächsten Zustand gilt" (NE**X**T)
- $F \dots$ "in der Zukunft gilt igrendwann" (**F**UTURE)
- $G \dots$ "in der Zukufnt gilt immer" (**G**LOBAL)
- $U \dots$ "es gilt eine Eigenschaft bis eine andere gilt" (**U**UNTIL)

Operator Präzedenz
- Unäre Operatoren: $\neg, G, F, X$
- Operator Until: $U$
- logische Operatoren $\land, \lor$
- Implikationsoperator $\rightarrow$

Auswertung von rechts nach links

## PROMELA
### Datentypen
- bit
- bool
- byte
- mtype (Eigene Konstanten definieren)
- short
- int

### Datenstrukturen
- Nur eindimensionale Arrays mit konstanter Länge möglich
- Mittels typedef eigene Datentypen definieren (keine Selbstreferenz möglich!)
- Mehrdimensionale Arrays können mittels eigenem Daentyp definiert werden
- Enumerations mit Hilfe von mtype (message type) möglich
- `mtype = {idle, busy, error}`
- Maximal 255 Labels möglich
- Labels werden intern auf Zahlen übersetzt
- Es kann maximal ein mtype pro Programm

### Nachrichtenkanälen
Intialisierung eines Kanals:

chan cname = [capacity] of {type1, ..., typeN}

- cname: Name der Kanalvariable
- capacity: Anzahl der Nachrichten, die im Kanal gespeichert werden können (capacity > 0: buffered channels)
- type: PROMELA Datentypen

Senden von Nachrichten über einen Kanal

cnam ! expr1, ..., exprN;

- expr1, ... exprN ist eine Sequenz von Ausdrücken deren Anzahl und Datentypen zur Initialisierung von cname passen muss

Empfangen von Nachrichten über einen Kanal

cname ? var1, ..., varN;

- var1, ..., varN ist eine Sequenz von Variablen deren Anzahl und Datentypen zur Initialisierung von cname passen muss

### Befehle
- `select(var: low .. high);`: Variable, Lower Bound .. Upper Bound
- `inline` functionName(param1, ..) {}: Inline Code
-

### Safety- und Liveness-Eigenschaften
- Safety: Ein schlechtes Ereignis $X$ tritt niemals ein
- Liviness: Ein gutes Ereignis $X$ tritt irgendwann einmal ein

### Prozess Scheduling
- Bis zu 255 Prozesse möglich, diese arbeiten nebenläufig
- Realisierung von Nebenläufigkeit auf nur einem Prozessor
- Scheduler wählt zufällig, aus welchen Prozess ein weiteres Statement ausgeführt werden soll
- Dadurch sind viele verschiedene Abläufe möglich
- nichtdeterministische Ausführung
- Ausführungen von Modellen sind entweder: unendlich, terminierend oder blockend
- Prozess Scheduling kann beschränkt/gesteuert werden durch
- Atomicity
- Fairness Anforderungen

#### Atomicity
- Ein Ausdruck oder Statement eines Prozesses welcher komplett ohne die Möglichkeit von Interleaving ausgeführt wird, heißt: atomar
- Zuweisungen, Sprünge, skip und Ausdrücke sind atomor
- Conditional expressions `(p -> q : r` sind atomar
- Guarded commands sind nicht atomar
- Erzwingbar durch `atomic`-Block

#### Fairness
Weak Fairness: Eine Programmausführung wird weakly fair genannt, falls die folgende Bedingung gültig ist:
- Falls ein Statement immer ausgeführt werden kann, dann wird es irgendwann als Teil der Programmausführung ausgeführt

## Spin
Never Claim: Spezifiziert einen Prozess der von Spin parallel zu jedem anderen Prozessschritt ausgeführt wird
- Wenn Ende erreicht ist, wird das Programm beendet und ein Fehler ausgelöst

never { /* p ist wahr in allen Zuständen*/

    do
    :: !p -> break
    :: else
    od
}

- Definition von Never Claims: LTL Formel oder seiteneffektfreier Promela Code (z.B. keine Zuweisungen)

LTL Formel
- Schlüsselwort `ltl`
-`ltl name formula`
- Unäre Operationen:
- `[], always`: Der zeitliche "immer gilt" Operator G
- `<>`: Der zeitliche "irgendwann gilt" Operator F
- !: Negation
- Binäre Operatoren
- U, until: Der zeitliche "es gilt bis" Operator U
- &&, ||: logisch und, oder
- /\,\/: Alternative Formen
- ->, implies: Implikation

## Büchi-Automat
$\omega$-reguläre Ausdrücke
- Sei $x$ ein regulärer Ausdruck, $L(x) \neq \emptyset$ und $\epsilon \not\in L$, dann ist $x^\omega$ ein $\omega$-regulärer Ausdruck
- $L(x^\omega) = L^\omega(x)$
- $x$ regulärer Ausdruck und $y$ $\omega$-regulärer Ausdruck
- Konktatenation ist $\omega$-regulärer Ausdruck
- $L(xy) = L(x) \cdot L(y)$
- $x, y$ $\omega$-regulärer Ausdruck, dann ist $x|y$ ein $\omega$-regulärer Ausdruck
- $L(x|y) = L(x) \cup L(y)$

Büchi-Automat $A = (M, R, q, E, \Sigma)$
- $M$ = Endlichen Menge an Zuständen
- $R \subseteq M \times \Sigma \times M$ = Relation
- $q \in M$ = Startzustand
- $E \subseteq M$ = Menge an Endzuständen
- $\Sigma$ = Eingabealphabet
- Unterschied zu DFA: Es muss midnestens einen Zustand geben, dass unendlich oft vorkommt

### TS in Büchi Automat
- Kanten und Knoten werden übernommen
- Aktionen und Labels an Knoten werden entfernt
- Füge neuen Startzustand "init" hinzu
- kanten enthalten Labels des Zielknoten
- Alle Knoten sind Endzustände

### Negationsnormalform
Alle Negationen sollen direkt vor atomaren Aussagen stehen

Umformungsregeln:
- $\neg\neg \varphi = \varphi$
- $\neg(\varphi_1 \lor \varphi2) = \neg \varphi_1 \land \varphi_2$
- $\neg(\varphi_1 \land \varphi2) = \neg \varphi_1 \lor \varphi_2$
- $\neg G\varphi = F \neg \varphi$
- $\neg F\varphi = G \neg \varphi$
- $\neg X \varphi = X \neg \varphi$
- $\neg(\varphi_1 U \varphi_2) = (\neg \varphi_1) R (\neg \varphi_2)$
- $\neg(\varphi_1 R \varphi_2) = (\neg \varphi_1) U (\neg \varphi_2)$
- Release Operator $\varphi_1 R \varphi_2 := \neg(\neg \varphi_1 U \neg \varphi_2)$

### Transformation LTL in Büchi Automaten
1. In Negationsnormalform bringen
2. Transformation in Graphen


Start des Algorithmus:
- Ist in einem Knoten das Feld "New" nicht leer, so wird der Knoten verfeinert oder ersetzt und die neu enstanden Knoten werden ebenfalls durch den gleichen Algoritmus verfeinert

Verfeinerungsregeln:

Ablauf:
- Starte mit einer leeren menge an "fertigen" Knoten
- Falls der aktuell betrachtete Knoten N ein leeres "New"-Feld besitzt
- Falls ein Knoten die gleichen "old" und "Next"-Felder besitzt wie N, dann wird N gelöscht und der Vorgänger von N dem "Incoming"-Feld des existierenden Knotens hinzugefügt
- Ansonsten wird der aktuelle Knoten N als "fertig" makiert und ein neuer Knoten als Nachfolger erstellt mit "Incoming" referenziert auf N, "New"-Feld enthält "Next"-Feld Inhalt von N
- Ansonsten wird eine Formel im "New"-Feld ausgewählt
- Ist diese im "Old"-Feld enthalten, löschen und Algorithmus auf den gleichen Knoten nochmal anwenden
- Ansonsten -> Verfeinerung

3. Transformation in Automaten
- Alphabet des Automaten: Potenzmenge alle atomaren Eigenschaften
- Zustände des Automaten: alle durch den Algorithmus erzeugten "fertigen" Knoten sowie der artifizieller Startzustand
- Zustandsübergänge: Übergänge von "Incoming"-Feldern, werden mit allen atomaren Eigenschaften beschriftet mit allen atomaren Eigenschaften, die die (ggf. negierten) atomaren Eigenschaften im "Old"-Feld des Zielknotens erfüllen. Falls "Old"- Feld leer, dann handelt es sich um einen "true" Übergang
- Anfangszustand: artifizieller Anfangszustand

Beispiel: $a U b$

## Prädikatenlogik
Signatur $\Sigma$ besteht aus
- Menge $T_\Sigma$ von Typen,
- Menge $F_\Sigma$ von Funktionssymbolen
- Menge $P_\Sigma$ von Relationssymbolen (Prädikaten)
- einer Typfunktion $\alpha_\Sigma$ mit $\alpha_\Sigma(p) \in T^*_\Sigma$ für alle $p \in P_\Sigma$ und $\alpha_\sigma(f) \in T^*_\Sigma \times T^*_\Sigma$ für alle $f \in F_\Sigma$
- Arität wird durch $f/n$ und $p/n$ angegeben, wobei $n$ die Arität von Funktions- und Relationssymbolen angeben

Ein Term des Typs $t \in T_\Sigma$ ist entweder
- eine Variable $v \in V$ des Typs $\alpha_\Sigma(v) = t$ oder
- ein Term $f(t_1, \dots, t_n)$ wobei das Resultat den Typ $t$ besitzt sowie alle Terme $t_i$ den korrekten Typ nach $\alpha_\Sigma(f)$ besitzen

Universum
- Eine nicht-leere Menge $D$ bezeichnet man als Universum. Jedem Element des Universums wird mit der Funktion $\delta: D \rightarrow T$ ein Typ zugewiesen.

### Evaluation

### Sequenzkalküle

## JML
- normal_behavior: Die aufgerufene Methode garantiert, dass keine Exception geworfen wird, falls die Vorbedingungen des Spezifikationsfalls erfüllt sind
- `requires`: Vorbedingung und boolesche Ausdrücke
- `ensures`: Nachbedingung und boolesche Ausdrücke
- `also`: Angeben von mehreren Spezifikationsfällen
- `\old(..)`: Zugriff auf Pre-Zustand
- `assignable`: Gibt an, ob sich Felder verändert haben
- `\nothing`: Nichts hat sich verändert
- `\everything``: Alles verändert sich
- Alternativ alle Felder notieren
- `public`: Spezifikation kann nur `public``Felder nutzen
- `spec_public`: Beibehalten von Sichtbarkeiten von Java und Zugriff auf nicht `public` Felder
- `pure`: Methode hat keine Seiteneffekte und terminiert immer
- `\created(...)`: Erzeugte Objekte
- `\result`: Nachbedingung bezieht sich auf den Rückgabewert der Methode
- `exceptional`: Ausnahme-Spezifikation erfordert, dass Methode eine Ausnahme wirft
- `signals_only`: Spezifiziert Typ der Ausnahme
- `signals`: Spezifiziert Post-Zustand, abhängig vom Typ der geworfenen Ausnahme (In Klammer spezifizieren, auf welchen Typ es sich bezieht), bspw `signals (E) b`
- `nullable`/`non_null`
- `loop_invariant`: Meistens folgendermaßen aufgebaut

/*@ loop_ivnariant
  @ (0 <= i && i <= a.length) &&
  @ (\forall int x; 0 <= x && x < i; condition);
  @ decreasing a.length - i
  @ assignable ...
  @*/

### Ausdrücke
- Negation: $!a$
- Logisches Und/Oder: $a && b$/$a || b$
- Implikation: $a ==> b$
- Äquivalenz: $a <==> b$
- Allquantor/Existenzquantor: (\forall t x; a)/ (\exists t x; a): "für alle Werte x des Typs t, a ist wahr"/ "es existier ein Wert x des Typs T sodass a"
- Bereichsprädikate: (\forall t x; a; b) = (\forall t x; a ==> b)