Assignable prevents proving the algorithm

[fab918]

Description

When I use "assignable" in the Key Editor, I have my proof which fails, yet the method does not modify anything. If assignable is removed, it works. This doesn't seem to limit to "\nothing", if I put array or array[*] it still doesn't work.

(I take advantage of this, is it possible to have more information on what is not working? I did not find any information on this subject, it is not clear where the problem lies)

Reproducible

yes

Steps to reproduce

public class Test {
    /*@ requires array != null && array.length > 0;
      @ ensures \result == (\sum int i; 0 <= i && i < array.length; array[i]);
      @ assignable \nothing;
      @*/
    public static int sum(int[] array) {
        int total = 0;
        
        //@ maintaining 0 <= i && i <= array.length;
        //@ maintaining total == (\sum int j; 0 <= j && j < i; array[j]);
        //@ decreases array.length - i;
        for (int i = 0; i < array.length; i++) {
            total += array[i];
        }
        return total;
    }
}

What is your expected behavior and what was the actual behavior?

pass the test

[mattulbrich]

Hi fab918, thanks for the report.

Try adding //@ assignable \nothing; to the loop specification (like above decrease). That should help.

[fab918]

@mattulbrich Thanks for your quick response.

I had tried the JML annotations loop_modifies and loop_writes but I had an error message in the import, I understood that it was not supported.

But yes it works with assignable, however it's not a JML standard, I just saw in the JML reference that it mentions that KeY uses assignable for loop.

Why isn't there an alias for loop_modifies, loop_writes, in order to be compatible with JML? It is kind of a shame not being able to have a common code for such a basic functionality when all it would take is an alias.

[mi-ki]

I had implemented such an alias some years ago, but apparently this did not survive the release cycles. Shouldn't be a problem to reintroduce it though, in my opinion.

[fab918]

@mi-ki Is there any trace of your contribution? I did a search on PRs but I don't see it.

[mi-ki]

@fab918 I just took a look, but found out I did not introduce an alias for loop_modifies or loop_writes, but for loop_variant and assigns (yet another standard from somewhere else, apparently). This was commit af97f72d1994cb50c74eb04c77649f198236f8ec. However, I am not sure whether their translation still works as it used to do, since many hard-to-follow things happened to the parser in-between.

[fab918]

@mi-ki Thanks, unfortunately I don't think it always works.

If anyone has any advice on how to get started, I'd love to hear it.

[mi-ki]

@fab918 I created a new branch which should hopefully fix the previously lost changes and also add the two keywords from OpenJML. Maybe, you can test whether it works for you?

[mi-ki]

It's been a while and after various internal discussions, the PR #3365 made it onto the main branch. So, @fab918, if you are still around, feel free to use it!