Bug updating state for statem post conditions about proper

[eiriniar]

This is actually not true. PropEr postconditions should be expressed in terms of the state prior to command execution (i.e. State, not State2).

The idea of "postcondition(S, C, Result) -> X" is to express constraints of the form:
when being in state S and performing call C, postcondition X should hold for the Result of the call.

[davisp]

Oh. Weird. Although I think I see what you mean. For instance, [1] is some code to test basical add/lookup operations on a btree. Currently the postcondition for the add call is checking that the KVs added are present in the state (which seemed reasonable and lead me to think proper had the bug).

Given your comment, it sounds more like I should really only be making assertions about Result in that call. Plus one could argue that the current thing is really testing dict more than the btree I think. Does that sound right?

[1] https://gist.github.com/1364115

[eiriniar]

I see what you mean, your assumption is reasonable. But then, it is also reasonable that you may want to check the Result of a call, given the context (i.e. state) in which that call was performed, not given the resulting state.
So in our approach, we assume that an error will be detected as an unexpected result of a call. Even if this is not captured
by a false postcondition right after the call, chances are high that it will become obvious sooner or later because of some state inconsistency. And then shrinking helps you identify it.

[davisp]

Yeah, I'm pretty sure I see the zen there. I just had my initial assumption and then looked at the code and saw the post condition being evaluated after the state was updated and assumed it was a bug. I just needed that slight tweak to my understanding of what postcondition was for. Thanks again.