[Java] \old() in loop-invariants

[Verwijderd]

Momenteel op de uni bezig met het leren van Java; daarbij de pre- en postcondities en invarianten in JML.

Nu wil ik een loop-invariant maken met daarin de JML-functie \old().

Bij bijvoorbeeld een postconditie in JML werkt dit prima, maar bij een loopinvariant krijg ik de volgende JML typecheck error in Eclipse (gebruikmakend van OpenJML):



Ik heb zo het gevoel dat \old() niet werkt in invarianten omdat deze functie de situatie vóór het aanroepen van een methode beschrijft, maar ik vermoedde dat zoiets ook wel zou gelden voor loops (dus: beschrijft de situatie voor het uitvoeren van de iteratie).

Iemand enig idee wat een mogelijke vervanging voor \old() kan zijn in een loop invariant?

Thanks!

Christian

[Verwijderd]

In de question en answer sessie van nu maar even gevraagd Conditie moet ook gelden aan het begin van de loop; da's natuurlijk niet zo.

[pedorus]

Hmm, hoeveel mensen zijn er eigenlijk die JML kennen? Bijna niemand: http://stackoverflow.com/questions/tagged/jml Gezien de leeftijd van die standaard zou ik zeggen dat het een beetje een dood kindje is. Misschien als ze het opnieuw zouden proberen met annotaties en meer aansluiting met junit dat het wat zou worden, maar ik vrees dat het nu vooral een theoretische tool is en blijft..

[Sebazzz]

Lijkt een beetje op Code Contracts in .NET op eerste gezicht?

[Verwijderd]

pedorus schreef op vrijdag 13 december 2013 @ 09:53:
Hmm, hoeveel mensen zijn er eigenlijk die JML kennen? Bijna niemand: http://stackoverflow.com/questions/tagged/jml Gezien de leeftijd van die standaard zou ik zeggen dat het een beetje een dood kindje is. Misschien als ze het opnieuw zouden proberen met annotaties en meer aansluiting met junit dat het wat zou worden, maar ik vrees dat het nu vooral een theoretische tool is en blijft..

Het is stof, dus zal het moeten gebruiken

Sebazzz schreef op vrijdag 13 december 2013 @ 09:56:
Lijkt een beetje op Code Contracts in .NET op eerste gezicht?

Klopt! Gaat inderdaad om programming by contract. Komt in feite op hetzelfde neer, alleen andere syntax.

[Kwistnix]

pedorus schreef op vrijdag 13 december 2013 @ 09:53:
Hmm, hoeveel mensen zijn er eigenlijk die JML kennen? Bijna niemand: http://stackoverflow.com/questions/tagged/jml Gezien de leeftijd van die standaard zou ik zeggen dat het een beetje een dood kindje is. Misschien als ze het opnieuw zouden proberen met annotaties en meer aansluiting met junit dat het wat zou worden, maar ik vrees dat het nu vooral een theoretische tool is en blijft..

Voor wat het waard is, ik doe nu 8 jaar hoofdzakelijk Java projecten en ik ben het in de praktijk inderdaad nog nooit tegengekomen. Neemt niet weg dat het voor educatieve doeleinden nog steeds zinnig kan zijn.