Hoare Axiome

  • Themenstarter Themenstarter BlackThorn
  • Beginndatum Beginndatum
B

BlackThorn

Guest
So Leute, jetzt het ich da mal eine Frage die wohl eher theoretischer Natur ist: Und zwar, kann mir jemand die Schleifeninvariante (Hoare Axiome) erklären? Hier ein Beispiel:

while (i <(n-1))
{
i++;
if (A < m) m = A else skip // skip ist eine Nulloperation, terminiert immer
}


so was wäre zum Beispiel bei dieser Schleife die Schleifeninvariante, und wie würde ich auf das kommen? Ich muss ehrlich sagen ich hab keine Ahung wie das funkt.

Danke BlackThorn
 
while (i <n-1))
{
i++;
if (A < m) m = A else skip // skip ist eine Nulloperation, terminiert immer
}


Also ich weiss net genau obs richtig ist abe es stimmt glaub ich

While (i<n-1) i ist ein zählvariable und n ist irgend eine variable die davor entweder durch eingabe oder irgenbd ein wert festgelegt worden ist.
ungefähr so
mache solange i kleiner n (irgendnezahl zb. 5) minus 1 ist. davor muss aber der startwertz von i festgerlegt sein.

i++ bedeztet ganz einfach das er beim nächsten durchlauf der schleife i um 1 erhöht.


if (A < m) m = A else skip
was aber genau in der abfrage steht verstehe ich net so ganz
das macht irgendwie kein Sinn
oder da fehlt das wörtchen then
weiss net obs so richtig ist aber i ist ein Element vom
Feld A und m ist wieder irgen ne Variable

if (A < m) then //wenn i element von Feld A < m ist

m = A dann ist m gleich i vom feld A

else skip //ansonsten hör auf wie schon oben steht skip ist eine Nulloperation, terminiert immer



das ist ohne denn rest des quelltextes schwer zu verstehen
 
Hm, danke *g* aber wie der Code funktioniert ist mir wohl klar, dies ist nicht so schwer, der such einfach nach dem kleinsten Element in der Liste.

Die Frage war nach der Schleifeninvariante. Inzwischen weis ich wie das funkt. Sie gilt immer vor, wärend und nach der Schleife.

Aber trotzdem danke!

Black Thorn
 
Original von Crash2key
while (i <n-1))
{
i++;
if (A < m) m = A else skip // skip ist eine Nulloperation, terminiert immer
}


[...]
das macht irgendwie kein Sinn
oder da fehlt das wörtchen then
Zum Vergrößern anklicken....


hm doch das macht sehrwohl einen sinn
und then fehlt erst recht nicht
denn so wie das stückchen code aussieht, ist das c.
aalso
was macht das?
in worten:

so lange, wie i kleiner n-1 ist
wird erst zu i eins dazugezählt, dann wird geprüft ob das element des arrays A mit der nummer i kleiner m ist, und wenn dem so ist wird m gleich diesem element gesetzt.
wenn das element nr. i nicht kleiner m ist, so wird die schleife abgebrochen.

noch fragen?
 
ok jetz mal zur auflärung

Mir gings hier nicht um den code ansich. Der Code und was er tut ist mir vollkommen klar. Die Anweisung skip steht nicht als c/java oder sonst ein befehl sondern ist ganz einfach allgemein gemeint, dass diese anweisung immer terminiert, also immer stimmt und immer beendet. Das muss nicht umbedingt eine "break" anweisung sein (übrigens break verwendet man möglichst nicht, das ist fast so wie ein label *g*) sondern kann auch irgendetwas anderes sein.

So worum gings: Also hier gings wie gesagt nicht um den Code ansich, sondern eigentlich um den Beweiss desselben, unzwar um den Beweiss dass er immer terminiert. Dies kann man mit den sogenannten Hoare - Axiomen / oder Tripel machen. Hier wollt ich die sogenannte Schleifeninvariante wissen. Diese gilt immer, also vor, nach und wärend der Schleife. In dem Fall wäre das dann:
{P} while B do S {Pand not B}
{m <= A ? i < n} while (i < (n-1)) do S {P and not B)}
P...Schleifeninvariante

So ich hoffe damit ist dieser Code wirrwar, und warum der geht, oder nicht geht geklärt!!

Cu, BlackThorn
 
Um antworten zu können musst du eingeloggt sein.
Zurück
Oben