nhatminhle
commented
8 years ago 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 notifications@github.com 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 https://github.com/nhatminhle/cofoja/issues/46.
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:
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?.