#129 assignable, working_space, & duration should be checked

[Dion Hinchcliffe]

My requires and assigned expressions in the JML
specifications always seem to work fine but I cannot
get the assignable, working_space, or duration fields
to work correctly. In other words, when I violate the
specification, no exception is thrown.

Here is the code I'm using. I would expect that
working_space and assignable would both throw exception
since I'm allocating 5000 booleans in my code as well
as assigning to visible fields that are not in my spec.

I know I"m doing something wrong but it seems pretty
straightforward that my call to 'foo()' is violating my
specification.

Thanks for your help!

Dion Hinchcliffe

public class JMLTestRunner {

public int member = 0;
public int onlyvalidreference = 0;

/*@ public normal_behavior
@ requires i > 0 && j > 0 && k > 0 && to != null;
@ ensures onlyvalidreference == 1;
@ assignable onlyvalidreference;
@ working_space 100;
@*/

public boolean[] foo(int i, int j, int k,
TestObject to)
{ boolean waste[] = new boolean[i];
if (onlyvalidreference != 1) { onlyvalidreference = 1; }
member = 1;
to.foo = 1;
return waste; }
/**
*
*/

public JMLTestRunner() {
super();
// TODO Auto-generated constructor stub
}

public static void main(String[] args) {
JMLTestRunner jtr = new JMLTestRunner();
try {
boolean[] mybools = jtr.foo(5000, 1, 1, new
TestObject());
System.out.println(jtr.member);
}
catch (Exception e)
{
System.out.println("*************
JMLEXCEPTION ************");
System.out.println(e);
e.printStackTrace();
System.exit(-1);
}
System.out.println("Done");
}
}

[Gary T. Leavens]

Logged In: YES
user_id=633675

Thanks for bringing this up, Dion. You are right that currently
these don't work, but it's no fault of your installation. These
features just currently aren't handled by jmlc. They require a
considerable amount of work, and we are trying to get
funding to do it. (Anyone is interested in picking up the ask,
however, if they would like to contribute.) So I'm sorry we
can't help with this for now. But this is a feature we would
like to have working