Beispiel operationale Semantik

Hintereinanderausführung:

C⟦c1;c2⟧=C⟦c2⟧ *C⟦c1⟧

C(x:=5;y:=1,σ) ->1 (y:=1, σ[5/x])->1σ[5/x][1/y]

Der -Kalkül ist relativ vollständig,

d.h. I={A} c {B} impliziert I- {A} c {B}.

S.208

schwächste Vorbedingung

----

s.1230

_____

eine Menge von Speicherbelegungen S.206

wpI [[c , B ]] =

{σ ∈ Σ I C [[c ]]σ |= I  B }

kann durch eine Formel arithmetisch dargestellt werden

--------

Beispiel für die Gültigkeit ⊨I B

B:= (a1=a2) := wahr/false

σ(I (a = a )) = true, falls σ(I (a )) = σ(I (a )), false, sonst.

a=n∋N/X∋Loc

σ(I (n)) = n für n ∈ N

σ(I (X )) = σ(X ) für X ∈ Loc

Ein Programmcode wird bezüglich einer Vorbedingung P und der Nachbedingung Q partiell korrekt genannt, wenn bei einer Eingabe, die die Vorbedingung P erfüllt, jedes Ergebnis die Nachbedingung Q erfüllt. Dabei ist es noch möglich, dass das Programm nicht für jede Eingabe ein Ergebnis liefert, also nicht terminiert.

Ein Code wird total korrekt genannt, wenn er partiell korrekt ist und zusätzlich für jede Eingabe, die die Vorbedingung P erfüllt, terminiert. Aus der Definition folgt sofort, dass total korrekte Programme auch immer partiell korrekt sind.

σ ⊨I A = σ(I(A))=true (S.167)

(a, σ) → n äq  A[[a]]σ = n

S.17

∅ ist Teilmenge jeder Menge

Hoare-Logik Zuweisungsregel

aus Nachbedingung wird Vorbedingung abgeleitet Alt. S.8-10

--------

Über Hoare Logik kann nur bewiesen werden, dass ein 

Programm korrekt arbeitet wenn es terminiert, nicht 

das es terminiert (partielle Korrektheit).

http://www.joern-stuphorn.de/de/syssafe/hoare/hoare-slides.pdf

----

Semantik von Programmen wird spezifiziert

Spezifikation beschreibt Verhältnis von Eingabe und  Ausgabe

Monotonie: Beweis vom Satz 5.24 altes Skript

S.5-24 :

wenn stetig => monoton

EinSpeicherzustand ist eine Funktion σ : Id→ Int  def. 3.7 altes Skript

Natürliche Ordinalzahlen

0 = ⊔∅. Null ist Limeszahl

eine weitere Limeszahl ist ω. Das ist die die grösser aler natürlichen Zahlen ist.

Damit ist N eine Wohlordnung ohne maximales Element, während N ∪ { ω } eine Wohlordnung mit maximalem Element ist.

⊥

∑ = ∑⋃{⊥}

C[[c]] :∑⊥ -> ∑⊥

C[[c]]σ =⊥ steht für C[[c]]σ undefiniert.

C[[c]]⊥=⊥

S.174 und 9-4 alt

Axiomatische Semantik

⊥ ⊨ false äq  ⊥ ( I ( false) = true (S. 174)

d.h. jeder boolesche Ausdruck von IMP ist auch eine

Zusicherung.

⊨ A heißt: Zusicherung A ist gültig, d.h. für beliebige

Werte der Programm- und freien Integervariablen ist die

Zusicherung wahr

⊨ X = k=>(X + X)<= 2*k

{true} skip {B} gdw B∈Assn eine wahre Aussage ist. (seite 164 Definotion von Assn)

Axomatische Semantik

Die axiomatische Semantik kann gut benutzt werden, um Verhalten von Programmen zu spezifizieren, wie schon in dem letzten Beispiel gezeigt wurde. swapxy( http://www.fh-wedel.de/~si/seminare/ws04/Ausarbeitung/9.AxiomatischeSemantik/ASemantik3.html )

Semantiksicht: Bedeutung von Anweisung c ist die Menge aller gültigen Korrektheitsaussagen { A } c { B }.

Das Beweissystem für partielle Korrektheitsaussagen (“Hoare-Kalkül”) besteht aus folgenden Regeln: lernen

Einzelschrittsemantik, Ergebnissemantik

a) Cmd × Σ →p Σ

Cmd x ∑: ausgangsgrad 1, eingangsgrad 1/0/unenflich viele

(jeder Zustand hat höchstens einen Nachfolger,

∑: ausgangsgrad 0, eingangsgrad 1/unenflich viele

End-

zustände haben keine Nachfolger)

b) Cmd × Σ →p Σ

Cmd × Σ : ausgangsgrad 1/0, eingangsgrad 0

∑: ausgangsgrad 0, eingangsgrad/unenflich viele

Zwischenschritte irrelevant, Semantik legt zu viele Details fest, nur Endzustände interessant!

Grundidee: Endzustände direkt durch Regeln definieren

----------

Ausführung von Anweisung c bei Speicherbelegung σ

terminiert mit Speicherbelegung σ′

: 〈 c,σ〉 ⇒σ′

------------

Gibt es σ′, so daß〈w2, σ〉 ⇒σ′ ?

Nein! Kein endlicher Ableitungsbaum möglich.

kleinste Fixpunkt:

Theorie der vollständigen Halbordnungen und stetigen Funktionen

Denotationale Semantik

Γb,c als Funktion b,c   in der auf der Grundmenge

(Σ →p Σ) definierten CPO mit f ⊑ g genau dann, wenn aus ”f(x) definiert“ folgt, dass auch g (x ) definiert ist und f (x ) = g (x ) gilt.

Bsp: ((A→p B),≤p) ist eine Halbordnung

f, g, h : {a,b,c}→p {1,2}

g:                 h:              f:

a->1            a->1         a->1

b->undef.   b->2         b->undef.

c->1             c->3         c->undef.

f ≤p h,

f ≤p g,

f ≤p g gdw.∀a∈ A: [ f(a) definiert ⇒g(a) definiert∧ f(a) = g(a) ]

-----

Da Γb,c stetig ist, wissen wir, dass der kleinste Fixpunkt existiert. Wir definieren nun C [[w ]] als den kleinsten Fixpunkt von Γb,c.Und wir definieren

w = while b do c od:

Korrektheit

Korrektheit bedeutet also, daß ein Algorithmus auch tatsächlich (für eine

beliebige Eingabe) das vorgegebene Problem löst.

http://www2.s-inf.de/Skripte/Progra.2000-WS-Lichter.(i3).Loesungen.pdf

Schwächste Vorbedingung wp

Für das Beispiel {P} x := 1 / y {x = 1 / y} gibt es viele Vorbedingungen, z.B. y < 0, y > 0, y > 5, y != 0, aber es gibt nur eine schwächste Vorbedingung:

y != 0

y > 0 und y < 0 sind beide stärker als y != 0, da beide y != 0 implizieren. Denn P ist per Definition schwächer als R, wenn R => P.
y<0 =>y!=0

y!=0 ⇏ y<=

Die axiomatische Spezifikation der Semantik des Sprachkonstrukts C

{P} C {Q}

gilt nur, wenn P die schwächste Vorbedingung für C und Q ist. Es gilt also:

{P} C {Q} nur, wenn P → wp(C, Q)

S.1230 Info II

Fixpunkt : f: X->X, wobei f(x)=x S.93

Der Nachweis der Korrektheit eines Programms kann jedoch nicht in allen Fällen geführt werden: das folgt aus dem Halteproblem bzw. aus dem Gödelschen Unvollständigkeitssatz. Auch wenn die Korrektheit für Programme, die bestimmten Einschränkungen unterliegen, bewiesen werden kann, so zählt die Korrektheit von Programmen allgemein zu den nicht-berechenbaren Problemen.

(eine Funktion berechenbar, wenn es einen Algorithmus gibt, der die Funktion berechnet)

Abbildung partiell total

Eine Abbildung f: M → N ordnet jedem a ∈ M höchstens

ein Element f(a) ∈ N zu. M heißt Vorbereich oder Urbild-

bereich (engl.: domain), N heißt Nachbereich oder

Bildbereich (eng.: codomain).

Wird hierbei jedem a ∈ M ein Element f(a) ∈ N zugeordnet,so heißt die Abbildung total.

Falls es möglich sein kann (aber nicht muss), dass manchen kein Element a ∈ M durch die Abbildung zugeordnet wird, so spricht man von einer partiellen Abbildung; man sagt dann, f(a) ist "nicht definiert" oder "undefiniert". Insbesondere fasst man jede totale Abbildung auch als partielle Abbildung auf.

--

jede totale Abb. ist partiell

Vollständigkeit (engl. completeness): Ist jede gültige partielle Korrektheitsaussage herleitbar?

⊨ { A } c { B } => ⊢ { A } c { B }

Gültigkeit der partiellen Korrektheitsaussage

⊨{A}c{B}

für ∀σ∈∑⊥ und für ∀ I:Intvar->N

Effektivität: Gibt es einen Algorithmus, der entscheidet, ob etwas eine Instanz einer Beweisregel ist?

Entscheidbarkeit: Gibt es einen Algorithmus, der entscheidet, ob eine Aussage{ A } c { B } gültig ist?

arithmetische Gültigkeit, d.h.

Aussagen sind für Standardinterpretation(Integerwerte,+,*,Konstanten) gültig.

Formale Semantik paralleler Prozesse S.229

Paralleloperator

neue Sprache IMPP

Aexp, Bexp bleiben

Cmd wird neu definiert (c1 II c2)

und Erweiterung der operationalen Semantik von IMP um vier Parallelausführungsregeln.

Die Semantik von IMPP liefert keine eindeutige Zuordnung eines

Endzustands zu einer Anweisung und einem Anfangszustand mehr.

Bsp.:X := 3 ∗ X + Y ∥ X := 17; Y := 1

Korrektheit (engl. soundness): Ist jede herleitbare

partielle Korrektheitsaussage gültig?

⊢ { A } c { B } => ⊨ { A } c { B }

-----

wenn jede wahre Aussage ableitbar ist.

http://de.wikipedia.org/wiki/Korrektheit_(Logik)

Nichtdeterminismus, S.232

Die Semantik von IMPP liefert keine eindeutige Zuordnung eines Endzustands zu einer Anweisung und einem Anfangszustand mehr.

Bsp.:X := 3 ∗ X + Y ∥ X := 17; Y := 1

c1 [] c2  entweder c1 oder c2

c1 II c2  sowohl c1 als auch c2 oder umgekehrt

Guarded Commands S.235

neue Sprache IMPGC:

Axp, Bexp, bleiben

Cmd wird verändert

GCmd neu definiert

Die operationale Semantik von IMPGC wird eingeführt (ähnlich der IMP) + Regeln für geschützte Anweisungen

Kommunizierende Prozesse S.241

paralel ausgeführte Prozesse tauschen ihre Daten über spezielle Kanäle: Chan

Input-Anweisung = Anforderung für eine Kommunikation

Labels stellen die tatsächlich erforderliche Kommunikation dar

Satz 5.2.2: Hoare Logik:

Die Regeln der Hoare Logik erzeugen nur korrekte Aussagen (partielle Aussagen):

⊢ { A } c { B } => ⊨ { A } c { B }

Die Verwendung dieser Seite ist nicht als thematisch geordnete Ansammlung von Informationen gedacht, sondern als ein mit Suchfunktion benutzes Notitzblatt