New annotation to indicate that method/function has no side-effects

[rtalexander]

Often times when writing a class there will be methods (i.e., accessors) whose only purpose is to return a value (e.g., getters and queries). In effect, the postcondition of such methods would be that the new values of all the state variables whose values could be changed have not been changed by the method. An obvious way to express this is simply enumerating all such variables:

@Ensures({
   "someVariable1 == old someVariable1)",
   "someVariable2 == old someVariable2)",
   ...
})

In many cases this approach would be impractical due to the shear number of mutable state variables available.

I would like to propose the addition of an additional annotation as a way to indicate that an accessor method has no side effects, such as @PreservesState (or a more appropriate name). Another way to do this would be to have an annotation that allows you to explicitly express what state variables are not changed, such as @Preserves({"stateVariable1","stateVariable2"}). This mechanism would allow easily allow you to express that there are no state side-effects as @Preserves("this").

Unlike the other annotations included with Cofoja, the proposed annotation would have no run time (or compile time) effect.

Thoughts?.

[nhatminhle]

I think this idea popped up sometime in the past. While immutability is a
desirable property to express and test, there's the issue of deep vs
shallow copying. To compare full states you need to clone the old object
entirely and then do a deep comparison. There is no simple way around that,
and if you are willing to go to such length, you can already do that with
@ensures("this.equals(old(this.clone()))") or something similar. This will
effectively run this.clone() on entry, save the result (the pointer to the
cloned object) and compare it using equals() to your instance when the
method is over.

In short: Unless I've missed something or there's a better way to implement
it that would be enabled by adding a new annotation, you should just use
@ensures I think.

Nhat

On Fri, Aug 14, 2015 at 8:51 PM, rtalexander [email protected]
wrote:

Often times when writing a class there will be methods (i.e., accessors)
whose only purpose is to return a value (e.g., getters and queries). In
effect, the postcondition of such methods would be that the new values of
all the state variables whose values could be changed have not been changed
by the method. An obvious way to express this is simply enumerating all
such variables:

@ensures({
"someVariable1 == old someVariable1)",
"someVariable2 == old someVariable2)",
...
})

In many cases this approach would be impractical due to the shear number
of mutable state variables available.

I would like to propose the addition of an additional annotation as a way
to indicate that an accessor method has no side effects, such as
@PreservesState (or a more appropriate name). Another way to do this
would be to have an annotation that allows you to explicitly express what
state variables are not changed, such as
@preserves({"stateVariable1","stateVariable2"}). This mechanism would
allow easily allow you to express that there are no state side-effects as
@preserves("this")

Thoughts?.

—
Reply to this email directly or view it on GitHub
#46.