---

Geschrieben von bavario am 14.11.2017 um 12:01:

  Hoare Logik (Gültigkeit von Triple beweisen)

Hallo zusammen. Ich steige noch nicht ganz hinter die Hoare Logik und habe hier ein paar Beispiele die ich nicht verstehe, vielleicht kann mir einer von euch ja weiter helfen? Beweisen Sie oder widerlegen Sie folgende Hoare-Triple:

1. {a > 7 und b >= 0} n = a - b {n < a und a + b >= 0}
Das müsste mit der Zuweisungsregel zu machen sein
Bzw ist das Tripple nicht gültig, da wenn a = 7 und b = 0 in der Vorbedingung gilt, gilt aber die Nachbedingung nicht, da n = 7 und 7 nicht echt kleiner 7 ist.

2.{x >= y + 1 und y ist gerade} z=x+2; x=x+y+z; {x gerade}
Da spielt die Hintereinanderausführung auf jeden Fall eine Rolle, aber wie wende ich das genau an? Welche Invariante wähle ich hier um ans Ziel zu gelangen?

3.{ x >= y + 1 und ygerade} if(0 != y%2){x=x+y;}else{z=x+2;x=x+y+z;}{ x gerade} Hier natürlich die if-Regel

Wäre toll wenn mir dabei jemand weiter helfen kann.
Beste Grüße