Hoarsche Regeln

Aus StudiWiki

[bearbeiten] Beispiel 1

while (x > 0) loop
    x := x - 1
end loop
--{x=0}

mit Zusicherungen

--{x>=0}
while (x > 0) loop
    --{x >= 1}
    x := x - 1
    --{x >= 0}
end loop
--{x>=0 and x<=0} daraus folgt {x=0}

die Invariante ist {x>=0}

[bearbeiten] Beispiel 2

y := 0
x := a
while (x > 0) loop
    y := y + 1
    x := x - 1
end loop
--{y = a}

mit Zusicherungen

y:=0
x:=a
--{y = 0 and x = a}

--{x+y = a and x >= 0}
while (x > 0) loop
    --{(x-1) + (y+1) = a} daraus folgt {x+y=a}
    y := y + 1
    --{(x-1)+y=a}
    x := x - 1
    --{x+y=a}
end loop
--{x+y=a and x>=0 and x<=0} daraus folgt {y=a}

invariante ist {x+y=a and x>=0}