Hoare in der Praxis?

[andras98]

Hi,

Wo bzw. wer verwendet den bitte den Hoare? Wo braucht man(n) den? Was beweise ich damit (klar die Gültigkeit) aber von was?

mfg

Andreas

[bla]

hab da auch ein problem damit.
in der prüfungsangabe vom 28.juni 2002 bsp3 zb:
dort steht:
Für die Invariante I wählen wir den Ansatz 3y = 2x+c, wobei wir c noch geeignet wählen m ussen.
Wie komm ich auf den ansatz der invariante I?
der rest ist mir relativ klar.
thx,
Klemens

[Jumper]

Wenn du so willst ist der Hoare die Erweiterung des Sequentialkalküls.... Bei der Assignment Language hast du das Problem, dass du Aussagen über dein Programm machen kannst, was du da gemacht hast. Das geht wunderbar in einer Konsequenzrelation dort hast du eine Vorbedingun P, eine Nachbedingung Q und dein Programm {a}, also P{a}Q. Somit kannst du beweisen, dass dein Programm mit der Vorbedingung P funzt und der Nachbedingung das ganze entspricht. Wie beid der Aussagenlogik ist dies ein semantisches Problem, welches du da vorliegen hast. Dies kannst du aber nicht ohne weiteres mittels einer semantischen Auswertungsfkt. lösen, da im Allgemeinen die Vorbedingungen aus Prämissen bestehen, die ein Abbild der derzeitigen Speicherbelegung sind. Also mußt du es syntaktisch lösen und da hilft dir der Hoare mit seinen Regeln, deswegen auch Kalkul, um deine Aufrufe wie begin a;b end syntaktisch zurückzuführen auf gewissen Invarianten bzw Formeln. Diese Inarianten und Formeln geben dir dann Rückschluß darauf ob dein Programm funktioniert oder nicht. Also einfach denn Formelhaufen wast herausgekriegt hast nehmen und schauen, das du irgendwie den linken Teil durch den rechten ausdrückst(wenn es eine Implikation ist) oder eine Konstante ausrechnest.
Der ganze Hoare also gibt dir Aufschluß ob deine Konsequenzrelation mit diesen Bedingungen und dem Programm funzt, ob es terminiert ist eine andere Frage.
Also in der Praxis wirst sowas net oft machen, weil selbst für ein kleines Programm ist da schon viel Arbeit drinnen, gerade weil jede Schleife eine Invariante liefert, und dass eben viel Arbeit bedeutet

[Jumper]

Diesen Ansatz bekommst du davon, dass deine Invariante für die Schleife zu wählen ist, die Invariante ist faktisch die Bedingung was eben in der Schleife gelten soll. Im Skriptum sind insgesamt 4 solche Möglichkeiten beschrieben, aus was so eine Invariante "entstanden" ist. Von wo du sie also abgeleitet hast entscheided dann, welche du wählst. Diese Invarianten im Skriptum sind nur Empfehlungen und das auch nur für die Nat. Zahlen.

Die Beschreibung dazu ist gleich im nächsten Absatz im Skriptum wo die Techniken beschrieben sind