 |
 |
 |
 |
 |
 |
Startseite » Forum » Beweis mittels Hoare-Kalkül
Beweis mittels Hoare-Kalkül
Universität / Fachhochschule
Tags: Beweis, hoare kalkül
 
|
  |
|---|
|
Hallo, das ist jetzt nicht 100% ein mathematisches Thema, aber sicher sollte das Hoare-Kalkül auch hier im Forum einigen Leuten ein Begriff sein :-) Ich habe folgendes kleiner Programm: {x >=0} // Vorbedingung a = x; y = 0; {a+y=x} // Nachbedingung Unter Nutzung der Regeln des Hoare-Kalküls möchte ich zeigen, dass aus der Vor- die Nachbedingung folgt. Ich habe ja nur zwei Zuweisungen. Wenn ich also die Zuweisungsregeln anwende, dann bekomme ich: {x >=0} // Vorbedingung {x+0 = x} // Anwendung der Zuweisungsregel a = x; {a + 0 = x} // Anwendung der Zuweisungsregel y = 0; {a+y=x} // Nachbedingung Ich müsste doch nun noch zeigen dass aus ich aus der Vorbedingung x+0 = x folgern kann, d.h.: {x >=0} --> {x+0 = x} Dann gilt {x >=0} --> {a+y=x} Oder liege ich hier völlig falsch? Für alle, die mir helfen möchten (automatisch von OnlineMathe generiert): "Ich möchte die Lösung in Zusammenarbeit mit anderen erstellen." |
| Hierzu passend bei OnlineMathe: |
|
|
Diese Frage wurde automatisch geschlossen, da der Fragesteller kein Interesse mehr an der Frage gezeigt hat.
|
1510023
1510023