[infostudents] Re: Rankingfunktion

  • From: Alexander Nutz <alex_nutz@xxxxxx>
  • To: infostudents@xxxxxxxxxxxxx
  • Date: Tue, 16 Sep 2008 21:28:37 +0200

Also gut..

Die Rankingfunktion ist ein Werkzeug um die Terminierung eines Programms zu beweisen. Mit dem Beweis der partiellen Korrektheit zusammen hat man dann totale gezeigt.
- es geht immer nur um die while-Schleife(n) in einem Programm -
Und das geht so:
Die Rankingfunktion rk muss folgende Bedingungen erfüllen:
- wenn sie unter null fällt, dann muss die while-Schleife abbrechen, also die Schleifenbedingung nicht mehr gelten.
- in jedem Durchlauf der Schleife muss ihr Wert abnehmen
formal heißt das:
für eine Invariante I und eine Schleifenbedingung B und einen Schleifenrumpf S

- rk < 0 => \not B
- {I and B and rk=x} S {rk<x}
- außerdem steht im olderog noch: {I} => rk >= 0 also die Invariante muss implizieren, dass die Funktion über null beginnt Ich glaube ich werde den Formalismus je nachdem variieren, wie sicher ich mich fühle - wenn's irgendwie nicht so gut klappt, kann man ja auch mit Worten argumentieren - das Prinzip ist ja eigentlich schon recht verstehbar...

kleines Beispiel

while (i>0)
i--;

hier würde man rk = i nehmen, würde ich sagen

while(i>a)
i--;

hier vielleicht rk=a-i

ich hoffe, das hilft dir.
alex



Michael Leukert wrote:
Kann jemand diese Rankingfunktion kurz erklären? War an dem Tag wohl nicht da und finde nichts auf google.
MfG,

Michael Leuket
---
Sent through the Infostudents Mailinglist

List Archive:
http://www.freelists.org/archives/infostudents/

Subscribe / Unsubscribe:
http://www.freelists.org/list/infostudents


---
Sent through the Infostudents Mailinglist

List Archive:
http://www.freelists.org/archives/infostudents/

Subscribe / Unsubscribe:
http://www.freelists.org/list/infostudents

Other related posts: