# Hoare Kalkül



## Guest (23. Mai 2005)

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 (24. Mai 2005)

Schonmal den Artikel von Wikipedia durchgelesen? 

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


----------



## Gast (25. Mai 2005)

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


----------



## Guest (29. Mai 2005)

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 (29. Mai 2005)

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])


----------

