accessible clauses for methods called in preconditions

[davidcok]

How should one think about the accessible-clause footprint for a method that calls a pure but not heap-free method in its precondition.

Perhaps the reads-footprint of methods called in specifications of Method M are ignored for method M's own footprint? After all, the reads-footprint of M contains all heap memory locations that affect the result and side-effects of M -- and anything called in specifications does not affect the result and side-effects.

That is the reads-footprint of a method only contains (a superset of) the locations read in the implementation, and not the specification.

And ditto for callable clauses. Except there we have to worry about termination, so perhaps callable clauses are more complicated. A non-terminating call in a specification would clearly be not-well-defined, but I at least have not thought about how to check/prove such termination (if it is even any different from termination of the implementation).

This does not arise for assignable clauses because they have to be pure in any case.

[leavens]

The key issue seems to be if we are including the specification in what a method can access. For that I agree that it's sensible to exclude the specification and only count what the method may access during its execution. I also agree with applying the same logic to callable clauses.

[mattulbrich]

Interesting question.Would be interesting to see an example with a sensible application of a specification that has a larger footprint than the implementation.

I have experimented with KeY and for example the follwoing is considered correct by KeY:

    int f;
    /*@ requires f == 0;
      @ ensures \result == f;
      @ accessible \nothing;
      @*/
    final int m() {
        return 0;
    }

whereas the accessible clause of the following cannot be proved:

    int f;
    /*@ requires f == 0;
      @ ensures \result == 0;
      @ accessible \nothing;
      @*/
    final int m() {
        return f;
    }

I have not really spent a lot of time on this, but I think your suggestion for reads clauses is sound.

[leavens]

It sounds like we are all agreeing to not count the read effects of a specification but only having read effects be part of what the method's code does.