[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:
//www.freelists.org/archives/infostudents/
Subscribe / Unsubscribe:
//www.freelists.org/list/infostudents
---
Sent through the Infostudents Mailinglist
List Archive:
//www.freelists.org/archives/infostudents/
Subscribe / Unsubscribe:
//www.freelists.org/list/infostudents
Other related posts:
