If statement with return in JML
i need to set up a postcondition which ensures to return null if size_ is 0. Based on
if(size_ == 0)
return null;
how can i do that in jml? any ideas? Following doesn't work:
//@ e开发者_开发问答nsures size_ == null ==> \return true;
thanks in advance
Try
//@ ensures size_ == null ==> \result == true;
Example:
//@ ensures size_ == null ==> \result == true;
public boolean sizeUndefined() {
if (size_ == null)
return true;
return size_.length() > 0;
}
You could also simply write it like this:
//@ ensures size_ == null ==> \result;
Here is the documentation for \result
:
3.2.14
\result
Within a normal postcondition or a modification target of a non-void method, the special identifier \result is a specification expression whose type is the return type of the method. It denotes the value returned by the method. \result is allowed only within an ensures, also_ensures, modifies, or also_modifies pragma that modifies the declaration of a non-void method.
First of all: what type is size_
, Object
or primitive(int)
?
Secondly, what the return type of the method? Object
or primitive(boolean)
?
You cannot compare a primitive type to null
, or return null
where a primitive type is supposed to be returned. If we assume size_
is int
and the return is boolean
then the the post-condition would be
//@ ensures size_ == 0 ==> \result;
精彩评论