Hoare Kalkül

  • 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.

  • 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?

  • 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)