[infostudents] Re: Rankingfunktion
- From: "Marius Greitschus" <greitsch@xxxxxxxxxxxxxxxxxxxxxxxxxx>
- To: <infostudents@xxxxxxxxxxxxx>
- Date: Tue, 16 Sep 2008 22:21:00 +0200
Kleine Korrektur:
while(i>a)
i--;
hier vielleicht rk=a-i
in diesem Beispiel wäre die Rankingfunktion
rk = i-a.
Da a kleiner ist als i (Invariante der While-Schleife), wäre die Funktion
bei Alex' Vorschlag immer kleiner 0. Darum i-a. Man kann sich auch merken:
Das größere minus das kleinere (für die Mathe-Dummköpfe, wie ich einer bin).
Aber Vorsicht: Immer darauf achten, was die While-Schleife macht. Wäre in
der Schleife ein i++; sähe die ganze Sache anders aus. (In diesem Beispiel
würde das Programm nicht terminieren und wäre damit nicht total korrekt.)
Ich hoffe, dass das jetzt noch geholfen hat und dass ich nicht zu großen
Blödsinn geredet habe.
Gruß,
Marius.
----- Original Message -----
From: "Alexander Nutz" <alex_nutz@xxxxxx>
To: <infostudents@xxxxxxxxxxxxx>
Sent: Tuesday, September 16, 2008 9:28 PM
Subject: [infostudents] Re: Rankingfunktion
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
---
Sent through the Infostudents Mailinglist
List Archive:
//www.freelists.org/archives/infostudents/
Subscribe / Unsubscribe:
//www.freelists.org/list/infostudents
Other related posts:
