FormalMethods05: Specification of resize()

Dear friends,

as I have said in class, one should not blame escjava2 too quickly.
Adding an implication prerequisite "number > 0" to the last part
of the specification of resize() makes the whole spec run through
the checker without problems ...

Please find the corrected version attached

Regards,
Wolfgang

Dear Klaus,

thank you for your feedback.

1. Please post in English, not all course participants understand German.

2. The use of the "News forum" is restricted in that only I can create a new thread. I have now created an additional "Discussions forum" which is open for everyone. You may use this for general discussions from now on.

3. You are right, JML only works with Java 1.4 (1.4.2 is the current version).
This is stated on the JML download page but I forgot to mention it and
did not refer to this page directly. The same will be true for
ESC/Java2 (I expect).

I will put some extra information on the "Software" pages.

Regards, Wolfgang

PS: please do not reply to this thread. I will start a new thread in "Discussions", please use that one.

Show parent | Reply

Leider sehe ich keine Möglichkeit einen neuen Thread zu eröffnen - vielleicht kann mir da ja einer von euch weiterhelfen.
Der ware Grund dieses Post ist, dass ich mich jetzt schon einen Tag mit JML gespielt habe bis ich es zum Laufen bekommmen habe.
Problem bei der Sache ist offensichtlich, dass JML nicht Java 1.5 kompatibel ist. Das Parsen der JML Spezifikation führt dabei beim Versuch JMLCompareable zu parsen zu einer java.lang.RuntimeException.
Mit Java 1.4.1_b02 scheint es zu funktionieren. Vielleicht kann ich so jemand anderem etwas Arbeit ersparen. Ein Hinweis beim Download wäre auf jeden Fall sinnvoll.

mfg
Klaus

Show parent | Reply