接口的 ContractInvariant 方法

Question

我是合同新手我浏览了代码合同的 msdn 文档

https://msdn.microsoft.com/en-us/library/dd264808(v=vs.110).aspx

我选择了契约不变量的想法。但是，当我添加不变方法时，它不会访问字段表单接口。

[ContractClass(typeof(Account_Contract))]
public interface IAccount
{
    int AccountID { get; }

    string AccountOwner { get; }

    int GetAccountID(); // Our 'internal'unique identifier for this account
}

[ContractClassFor(typeof(IAccount))]
internal abstract class Account_Contract : IAccount
{
    int IAccount.AccountID
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() > 0);
            return default(int);
        }
    }

    string IAccount.AccountOwner
    {
        get
        {
            Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
            return default(string);
        }
    }

    int IAccount.GetAccountID()
    {
        Contract.Ensures(Contract.Result<int>() > 0);
        return default(int);
    }
}

它工作正常，但如果我添加

Contracts.Requires(AccountID > 0);

VS 不访问它。我也试过

Contracts.Requires(this.AccountID > 0);
Contracts.Requires(IAccount.AccountID > 0);

None 正在工作。我哪里做错了。

Answer 1

你的问题是你正在使用显式声明（因为@Chris 在他的回答中有评论），所以你必须将 this 转换为 IAccount.

我认为你应该使用隐式声明（常用），因为IAccount实现的所有方法和道具必须public。

隐式声明方式：

[ContractClassFor(typeof(IAccount))]
internal abstract class Account_Contract : IAccount
{
    //In order to implement IAccount interface, must be public
    public int AccountID
    {
        get
        {
            Contract.Requires(AccountID > 0);
            return default(int);
        }
    }

    //In order to implement IAccount interface, must be public
    public string AccountOwner
    {
        get
        {
            Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
            return default(string);
        }
    }

    //In order to implement IAccount interface, must be public
    public int GetAccountID()
    {
        Contract.Ensures(Contract.Result<int>() > 0);
        return default(int);
    }
}

[ContractClass(typeof(Account_Contract))]
public interface IAccount
{
    int AccountID { get; }

    string AccountOwner { get; }

    int GetAccountID();             ////Our 'internal'unique identifier for this account
}

编辑：我在这里包括@Cris 的回答。

显式声明方式：

[ContractClassFor(typeof(IAccount))]
internal abstract class Account_Contract : IAccount
{
    int IAccount.AccountID
    {
        get
        {
            //You must cast this as IAccount
            Contract.Requires(((IAccount)this).AccountID > 0);
            return default(int);
        }
    }

    string IAccount.AccountOwner
    {
        get
        {
            Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
            return default(string);
        }
    }

    public int GetAccountID()
    {
        Contract.Ensures(Contract.Result<int>() > 0);
        return default(int);
    }
}

Answer 2

您正在使用接口的显式实现，这意味着如果您想将对象视为该接口的成员，那么您需要先转换为该接口。

因此，当您想要访问名为 myInstance 的实例上的 AccountID 时，您需要编写 ((IAccount)myInstance).AccountId。如果您尝试直接在 class 上访问 AccountId，那么它不会被识别。

这意味着如果您需要从 class 中为您的合约引用它，您应该使用 ((IAccount)this).AccountId.

虽然处理这个问题的更简单方法是隐式实现接口，但事情会一直更自然一些。要隐式实现该接口，只需从其声明的开头删除 IAccount. 即可。有关隐式和显式接口的更多信息，请参阅 C# Interfaces. Implicit implementation versus Explicit implementation .

接口的 ContractInvariant 方法

ContractInvariant method for interface

c#

inheritance

code-contracts

隐式声明方式：

显式声明方式：