Hoare Kalkül

[Guest]

Ich beschäftige mich grad mit dem Thema, also partielle Korrektheit, totale Korrektheit, Hoare-Kalkül.
Seh dort aber noch nicht recht durch.
Kennt ihr vllt. ein paar Internetseiten, wo das gut erklärt wird(etwas genauere Erklärungen zu den einzelnen Regeln wie Zuweisungsregel etc.)

 

[mic_checker]

Schonmal den Artikel von Wikipedia durchgelesen?

Gibt es evtl. konkrete Fragen die man beantworten könnte?

 

[Gast]

danke, das hilft mir erstmal.
Zwecks weiterer Fragen, meld ich mich dann nochmal.

 

[Guest]

so jetzt muss ich nochmal was fragen und zwar möchte ich nun die folgende Methode auf totale Korrektheit überprüfen.
Die Methode gibt das kleinste Element eines arrays zurück.
Aber es scheitert schon daran ein geeignetes Prädikat für eine Nachbedingung und eine Vorbedinung zu finden/definieren.

static int minElement(int[] arr) 
{
	int n=arr.length;
	int min=arr[0];
	int i;
	i=1;
	while (i<n) 
        {
             if (min > arr[i]) min = arr[i];
	    i++;
	}
	return min;	
}

//PRE:
n>=0 (denn das array kann keine negative Länge haben)
muss nun weiterhin gelten, dass das bis dato "kleinste" Element des arrays, das erste Elemnt ist (min=arr[0])???

//POST:
hier weiß ich sorecht garnicht wie ich das formulieren soll.
min=j mit j€[0,arr.length-1] AND j<arr[j+1] <-- Blödsinn oder?

kann mir wer helfen eine geeignete logische Aussage über die Nachbedingung/Vorbedingung zu formulieren?

 

[Bleiglanz]

deine nachbedingung ist käse, du gibts ja nicht den index des kleinsten elements zurück, sondern das kleinste element selber

// pre
n >= 1 (den auch ein leeres array kann kein kleinstes haben)

// post
min <= arr[j] für j=0...n-1
UND
es gibt ein j mit (0 <= j <= n-1 und min=arr[j])