C# 代码契约：从其他线程访问成员的后置条件是否无用？
经过一番思考，我得出的结论是，方法中的后置条件仅在强加于返回值、ref 和 out 参数时才有用，但不适用于字段、静态或任何实例。原因是，当调用该方法时，该调用的静态分析无法对字段上的后置条件执行任何操作，因为其他线程可能已经将该字段更改为任何状态，因此不一定满足后置条件。我的结论是，对多个线程可访问的任何内容（基本上只是字段）施加的后置条件是无用的，并且只留下后置条件对返回值以及 out 和 ref< 的用处。 /em> 参数。不变量是字段后置条件的唯一形式，不会被线程否定。
我问这个推理是否错误，以及我是否缺少字段后置条件的任何非元目的的参数。我所说的“元”是指任何可以通过其他方式完成的东西，特别是通过评论。
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 postcondition. 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.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
它可以确保你已经满足了他们。如果另一个线程更改了字段的值，使得当您返回后置条件不成立时，则您的类将按照其线程安全规范以线程不安全的方式使用（否则它将实现同步设施以提供线程安全）从一开始就可以阻止这种情况的发生）。你在这里所说的是“如果你以类不支持的方式使用类，那么后置条件就没有帮助”。但在这种情况下，这是您最不用担心的。
用于后置条件的相同参数也可用于类不变量：其他线程可能已开始修改该对象并将其置于不一致的状态（只要执行该操作的公共方法尚未返回，它们就可以这样做），因此当你返回时，不变量不成立。
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 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.