Hoare Kalkül

[JanThomas]

Kann mir jemand verraten, wie ich auf die Schleifeninvariante im Hoare-
Kalkül der letzten VO-Prüfung komme?

Das Beispiel lautete wie folgt:

z = 15 {begin begin x <-- 5z; y <-- z+x end;
while y>=4 do begin y <-- y - 4; x <-- x+3 end end} x = 141

Danke.

[Chuck]

mhm das is jetzt reine spekulation ... aber hast dus schon mit
3y+4x=c für eine beliebige konstante c versucht?
so ist diese art von schleife im skriptum aufgelöst worden

[MindSeeker]

also erst mal... der vorschlag mit der invariante funktioniert.
INV: 4x + 3y = 570

allerdings ...puh solche beispiele kosten zeit! für wie groß haltet ihr die wahrscheinlichkeit, dass er sowas gibt?

[Chuck]

also ich würd sagen die bsps dauern ned so lang wie zb die sprache die ein dea beschreibt herauszufinden oder einen dea aus einer verbalen beschreibung zu generieren

insofern würd ich mich eher über ein solches bsp freuen :)

mit den hilfen die im skriptum gegeben sind sollt das finden von invarianten relativ gut gehen, da er sicher keine bsps geben wird, die irgendwie komplett vermurkste inv s benötigen

ich denke mal sowas könnt schon kommen (wohl genauso wahrscheinlich wie das ganze andere zeug zu logik und sprachen)