JML und \forall (oder andere Funktionen)

Benutzeravatar
mansur
Windoof-User
Windoof-User
Beiträge: 30
Registriert: 14. Okt 2007 02:21

JML und \forall (oder andere Funktionen)

Beitrag von mansur »

Hallo,

Mal eine generelle Frage. Hoffe ich hab nichts übersehen..
In den Folien ist es immer so, dass z.B. bei einer Sortierung in dem Bedingungsbereich nur einfache Vergleiche gemacht werden:

Code: Alles auswählen

/*@ ensures (\forall int i, j; i >= 0 && i < j && j < size; arr[i] < arr[j]); @*/
Mein Ansatz ist dann aber immer eine Variable zu sparen wie folgt:

Code: Alles auswählen

/*@ ensures (\forall int i; i <= 0 && i < size - 1; arr[i] < arr[i+1]); @*/
Ist es denn überhaupt erlaubt "size - 1" oder sogar andere Funktionen in der Bedingung zu benutzen? Gehe eigentlich davon aus...

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: JML und \forall (oder andere Funktionen)

Beitrag von Nathan Wasser »

Das ist erlaubt, ja. In diesem Fall ist es auch kein Problem, da die Transitivität von < dafür sorgt, dass die Formeln äquivalent sind. Manchmal wäre das aber nicht möglich.

Antworten

Zurück zu „Archiv“