Hoare Logik (Gültigkeit von Triple beweisen) |
| 14.11.2017, 12:01 | Auf diesen Beitrag antworten » |
| bavario | 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 |
|
|
|
|
|
Verwandte Themen
| Die Beliebtesten » |
|
| Die Größten » |
|
| Die Neuesten » |
|
