postcondition problem Beetlz - BON - JML checking

kiniry / Mobius

4 stars 8 forks source link

postcondition problem Beetlz - BON - JML checking #599

Open atiti opened 11 years ago

atiti commented 11 years ago

Here is another example :

BON specification :

deferred processArray: SEQUENCE[INTEGER] require mod_name /= Void; ensure Result /= Void; end

corresponding message after checking:

Multiple markers at this line

processInputStream@ICHANNEL is missing postcondition: Result /= Void
processInputStream@ICHANNEL expected MIXED but found QUERY.

Problem is : I have already specified postcondition Result /= Void; Also is not clear : meaning of MIXED ( How to ? )

atiti commented 11 years ago

From: evka (GH: EvkaD) Date: Sun Nov 8 10:23:05 2009

from what it looks like the error message is talking about the method processInputStream, which is not the one in the example. Can it be that the error message was attached to the wrong line?

The message about the method as expected MIXED comes from the Java method being both query and command, whereas in BON this is not (should not) be allowed. A query is a pure method with non-void return value, i.e. either specified as pure or specified as @assignable \nothing. A command is a method with void return value.