Korrektheitsaussagen

Assignment Language über Z\small \Z

Assigned Languge für Datentyp D\mathcal D

Syntax (Wiederholung)

AL(D)\small AL(\mathcal D ) ist die kleinste Menge für die gilt

  1. v←‾t∈AL(D)v \underline \larr t \in A L(\mathcal{D})

    wenn v∈IVSv \in I V S und t∈T(D)t \in \mathcal{T}(\mathcal{D})

  1. begin‾α; βend‾∈AL(D) \underline{\text{begin}}~ \alpha \text {; } \beta ~\underline{\text{end}} \in A L(\mathcal{D}) 

    wenn α,β∈AL(D)\alpha, \beta \in A L(\mathcal{D})

  1. if‾Bthen‾αelse‾β∈AL(D) \underline{\text{if}}~ B ~\underline{\text{then}}~ \alpha ~\underline{\text{else}}~ \beta \in A L(\mathcal{D}) 

    wenn α,β∈AL(D)\alpha, \beta \in A L(\mathcal{D}) und B∈BA(D)B \in \mathcal{B} \mathcal{A}(\mathcal{D})

  1. while‾Bdo‾α∈AL(D) \underline{\text{while}}~ B ~\underline{\text{do}}~ \alpha \in A L(\mathcal{D}) 

    wenn α∈AL(D)\alpha\in A L(\mathcal{D}) und B∈BA(D)B \in \mathcal{B} \mathcal{A}(\mathcal{D})

Syntax (überZ\small \Z)

Programme

AL→Var⁡ “←" Term∣ \small A L \rightarrow \operatorname{Var} \text{ ``}\leftarrow\text {" Term} \mid 

 “begin" AL “;" AL “end" ∣\small \text { ``begin" AL ``;" AL ``end" } \mid

 “if" Cond “then" AL “else" AL∣ \small \text { ``if" Cond ``then" } A L \text { ``else" } A L \mid 

 “while" Cond “do" AL \small \text { ``while" Cond ``do" AL }

Boolsche Ausdrücke

Cond → “(" Term BinRel Term “)" | “(" Cond LogOp Cond “)" | “ ¬" Cond \small \text {Cond } \rightarrow \text { ``(" Term BinRel Term ``)" | ``(" Cond LogOp Cond ``)" | ``} \neg \text{" Cond} 

BinRel →‘‘="∣‘‘≠"∣‘‘>"∣"≥‘‘∣‘‘<"∣‘‘≤" \small \text {BinRel } \rightarrow ``="\mid ``\neq "\mid ``>"\mid " \geq ``\mid ``<" \mid ``\leq " 

LogOp→‘‘∧"∣‘‘∨" \small \text{LogOp} \rightarrow `` \wedge " \mid `` \vee " 

Arithmetische Ausdrücke

Term → Var ∣ Const ∣‘‘(" Term BinOp Term “)" \small \text {Term } \rightarrow \text { Var } \mid \text { Const } \mid ``(" \text { Term BinOp Term ``}) " 

BinOp⁡→‘‘+"∣‘‘−"∣‘‘∗" \small \operatorname{BinOp} \rightarrow ``+"\mid``-"\mid ``* " 

Const →‘‘0"∣‘‘1"∣‘‘2"∣⋯∣‘‘42"∣⋯ \small \text {Const } \rightarrow ``0" \mid ``1" \mid ``2" \mid \cdots \mid ``42" \mid \cdots 

Var⁡→‘‘x"∣‘‘y"∣⋯∣“irgendeinWort"∣⋯ \small \operatorname{Var} \rightarrow ``x" \mid ``y" \mid \cdots \mid \text{``irgendeinWort}" \mid \cdots 

Semantik (überZ\small \Z)

M(l,v←t)=I′\small \mathcal{M}(l, v \leftarrow t)=I^{\prime}

wobei I′(v)=M(I,t)\small I^{\prime}(v)=\mathcal{M}(I, t) und I′∼vI\small I^{\prime} \stackrel{v}{\sim} I

M(I, begin α;β end )=M(M(I,α),β) \small \mathcal{M}(I, \text { begin } \alpha ; \beta \text { end })=\mathcal{M}(\mathcal{M}(I, \alpha), \beta) 

M(I, if B then α else β)={M(I,α) falls M(I,B)=tM(I,β) falls M(I,B)=f \small \mathcal{M}(I, \text { if } B \text { then } \alpha \text { else } \beta)= \begin{cases}\mathcal{M}(I, \alpha) & \text { falls } \mathcal{M}(I, B)=\mathbf{t} \\ \mathcal{M}(I, \beta) & \text { falls } \mathcal{M}(I, B)=\mathbf{f}\end{cases} 

Vereinfachungen

Keine Unterscheidung zwischen Syntax und Semantik

Keine Unterscheidung zwischen unterschiedlichen Meaning-functions zum Auswerten:

M\small \mathcal M ersetzt MAL,MBA,MT \small \mathcal{M}_{A L}, \mathcal{M}_{\mathcal{B A}}, \mathcal{M}_T 

Datentyp / Modellstruktur bleibt fix Z\small \Z .

Korrektheit

Spezifikation

Korrektheit: "Programm tut was es tun soll"

Benötigt formale / mathematisch-logische Spezifikation des Verhaltens.

AL( Z\small \Z ) hat Prädikatenlogik als Spezifikationssprache

Formel

Jede Formel F\small F repräsentiert {I∈ENV∣M(I,F)=t}\small \{I \in E N V \mid \mathcal{M}(I, F)=\mathbf{t}\} alle Wertebelegungen, in denen sie wahr ist.

Beispiel: ∃i(x=2i)\exists i(x=2 i)

repräsentiert alle Wertebelegungen I\small I in denen I(x)\small I(x) eine gerade Zahl ist.

Korrektheitsaussage

Korrektheitsaussage = Programm + Spezifikation

{\small \{ Vorbedingung }\small \} = Programm + {\small \{ Nachbedingung }\small \}

{\small \{ PL-Formel }\small \} = AL( Z\small \Z ) + {\small \{ PL-Formel }\small \}

{\small \{ F }\small \} = α\small \alpha + {\small \{ G }\small \}

Wahrheit einer Korrektheitsaussage{F}α{G}\small \{F\}\alpha\{G\}

Eine Korrektheitsaussage ist wahr, wenn jede zulässige Eingabe zum richtigen Ergebnis führt.

Wenn eine Wertebelegung die Vorbedingung erfüllt, dann erfüllt die Wertebelegung bei Programmende die Nachbedingung .

∀I∈ENV:M(I,F)=t⟹M(I′,G)=t \small \forall I \in E N V: \mathcal{M}(I, F)=\mathbf{t} \implies \mathcal{M}\left(I^{\prime}, G\right)=\mathbf{t}  wobei I′=M(I,α)\small I^{\prime}=\mathcal{M}(I, \alpha)

Wahrheit einer Korrektheitsaussage bezüglich...

  1. Partielle Korrektheit

    Falls die Eingabe zulässig ist, ist das Ergebnis richtig wenn das Programm terminiert.

    ∀I∈ENV:M(I,F)=t⟹M(I′,G)=t \small \forall I \in E N V: \mathcal{M}(I, F)=\mathbf{t} \implies \mathcal{M}\left(I^{\prime}, G\right)=\mathbf{t} wennI′=M(I,α)\small I^{\prime}=\mathcal{M}(I, \alpha) definiert ist

  1. Totale Korrektheit (= Partielle Korrektheit + Termination)

    Falls die Eingabe zulässig ist, ist das Ergebnis richtig und das Programm terminiert.

    ∀I∈ENV:M(I,F)=t⟹M(I′,G)=t \small \forall I \in E N V: \mathcal{M}(I, F)=\mathbf{t} \implies \mathcal{M}\left(I^{\prime}, G\right)=\mathbf{t} undI′=M(I,α)\small I^{\prime}=\mathcal{M}(I, \alpha) ist defniert

Beispiele (ohne Hoare-Kalkül)