不变方法 [ContractInvariantMethod] 可以在接口契约中工作吗?

发布于 2024-11-30 14:41:28 字数 925 浏览 3 评论 0原文

我正在创建接口合同,如 2011 年 2 月 4 日代码合约用户手册(PDF)。这不是问题。

另外,我想将对象不变性(参见§4.2 ContractInvariantMethod)混合到同一个接口契约中。这是一个问题。我找不到在接口契约上使用对象不变量的示例。

我尝试将对象不变式添加到接口契约中,如以下部分代码片段所示。它编译。在运行时它不会引发任何错误,但它似乎也没有做任何积极的事情(即被调用)。

/* Note: The intention of this snippet is to cause the data implementation
 * to fail if it is not initalized before its public data access methods are called. 
 */
[ContractClassFor(typeof(IDataProxy))]
abstract class IDataProxyContract : IDataProxy
{
    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(IsInited == true, "Instance not initialized.");
    }

我找不到专门解决这种情况或反驳这种情况的文档。

此时,我不确定是否错过了使其工作的步骤,或者代码契约技术是否完全忽略了此上下文中的对象不变式。我想让它发挥作用。有人知道答案吗?

I'm creating an Interface Contract as described in § 2.8 Interface Contracts of Feb 4, 2011 Code Contracts User Manual (PDF). This is not a problem.

Additionally I want to mix an Object Invariant (see § 4.2 ContractInvariantMethod) into the same Interface Contract. This is a problem. I cannot find examples of Object Invariants being used on Interface Contracts.

I tried adding an Object Invariant to the Interface Contract seen in the following partial code snippet. It compiles. At runtime it doesn't raise any errors, however it doesn't appear to do anything positive (i.e. be invoked) either.

/* Note: The intention of this snippet is to cause the data implementation
 * to fail if it is not initalized before its public data access methods are called. 
 */
[ContractClassFor(typeof(IDataProxy))]
abstract class IDataProxyContract : IDataProxy
{
    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(IsInited == true, "Instance not initialized.");
    }

I can't find documentation that specifically addresses this scenario or refutes it.

At this point I'm unsure if I'm missing a step to make it work, or if Code Contract technology ignores the Object Invariant in this context altogether. I would like to make it work. Does anybody know the answer?

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(3

╰◇生如夏花灿烂 2024-12-07 14:41:28

显然,答案在 DevLabs 论坛中,由 Microsoft (MSFT) 的 Manuel Fahndrich 回答:

接口目前不支持对象不变量。我可以
看看为什么它们可能很方便。

完整上下文和代码示例位于此处...

Apparently the answer is in the DevLabs forum answered by Manuel Fahndrich, Microsoft (MSFT):

Object invariants are not supported on interfaces at the moment. I can
see why they might be handy though.

Full context and code sample here...

如何视而不见 2024-12-07 14:41:28

它们默认处于关闭状态。

我的猜测是,编译器选项未启用合约,因此它们不会被编织到代码中。

下载此软件包

安装后,转到项目属性,您将看到另一个选项卡。

然后,您可以启用一个选项:“执行运行时合同检查:完整”

They are off by default.

My guess is that the contracts are not enabled by the compiler options, so they don't get weaved into the code.

the solution is to download this package from devlabs

after you install it, go to the project properties, and you'll see another tab.

then, you can enable an option: "Perform runtime contract checking: full"

萌化 2024-12-07 14:41:28

不变量提供了一种约束对象内部状态的机制。

它们被视为实现细节,这就是它们在私有方法内实现的原因。接口显然没有状态的概念(甚至属性只是方法的语法糖),因此不能有不变量。在其最原始的用途中,不变量用于字段。然而,自动属性的概念显然模糊了这条界限,导致本例中出现混乱。

我同意应该有一种更简洁的方式来承包财产,因为您的前置条件和后置条件总是相同的。

Invariants provide a mechanism for constraining the internal state of an object.

They are seen as implementation details which is why they are implemented inside a private method. Interfaces obviously have no concept of state (even properties are just syntactic sugar for methods), and consequently cannot have invariants. In their most primitive use, invariants are used on fields. However, the concept of automatic properties has obviously blurred this line, leading to confusion in this case.

I agree there should be a more concise way of contracting properties, simply because your pre and post conditions are invariably going to be the same.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文