C# Code Contracts: Are postconditions on members accessible from other threads useless?

after some thinking I have concluded that postconditions in methods are useful only when imposed on the return value, ref and out parameters, but not on fields, neither static nor on any instance. The reason is that when that method is called, static analysis of that call can't do anything with postconditions on a field, because other threads might have already alter that field to any state, and therefore not necessarily meeting the postco开发者_运维问答ndition. I conclude that postconditions imposed on anything accessible by more than one thread, which are basically only fields, are useless, and that leaves only the usefulness of postconditions on the return values and out and ref parameters. The invariant is the only form of postconditions on fields not negated by threading.

I'm asking whether this reasoning is faulty and whether I'm missing arguments for any non-meta purpose of postconditions on fields. With 'meta' I mean anything which could also be accomplished by other means, in particular by commenting.

---

static analysis of that call can't do anything with postconditions on a field

It can make sure that you have satisfied them. If another thread changes the value of a field such that when you return the postcondition does not hold, then your class is being used in a thread-unsafe manner as per its thread safety specification (otherwise the sync facilities it would implement to provide thread safety would have prevented this from happening in the first place). What you 're saying here is "if you use the class in a manner it does not support being used in, then postconditions don't help". But that's the least of your worries in this case.

The invariant is the only form of postconditions on fields not negated by threading.

The same argument you used for postconditions can be used for class invariants: other threads may have started modifying the object and left it in an inconsistent state (they can do so as long as the public method that does it has not returned), so that when you return the invariant does not hold.