---

Geschrieben von energyfull am 16.01.2009 um 23:33:

  Hoare-Formel

hi informatiker,ich hätte da eine frage, wie ich eine hoare-formel für die berechnung der funktion f(x)=x² angeben kann??

---

Geschrieben von kiste am 17.01.2009 um 13:35:

 

Ich habe bei Google nur gefunden dass eine Hoareformel einfach ein {P}c{Q} ist. Dann kannst du doch {true} y= x*x; {y=x^2} benutzen oder hab ich was falsch verstanden?

---

Geschrieben von energyfull am 17.01.2009 um 20:10:

 

ich bin mir da auch nicht so sehr sicher, deshalb war ja meine frage

---

Geschrieben von energyfull am 18.01.2009 um 13:01:

 

ich habe da noch eine frage:

ich habe einen pseudocode:

proc calc (x,n) {
i := 0;
p:= 1;
s:= 1;
while < n do
i:= i+1;
p:= p*x;
s:= s+p;

od
print s;
}


kann mir einer erklären was diese funktion berechnet? und wie man die totale korrktheit der funktion bzgl. der behauptung nachweist?

---

Geschrieben von kiste am 18.01.2009 um 16:09:

 

Falls es while i < n heißt wird hier dann berechnet. Das kannst du z.B. mit einer geeigneten Schleifeninvariante zeigen.

---

Geschrieben von energyfull am 18.01.2009 um 23:03:

 

ja es soll i<n heissen, wie zeigt man denn so was? kannst du mir helfen?

und was ist denn mit der totalen korrektheit?