[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:
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


---
Sent through the Infostudents Mailinglist

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

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

Other related posts: