为什么可以为后置条件和对象不变量添加和删除代码契约，但不能为 C# 中的前置条件添加和删除代码契约？

Question

为什么可以为后置条件和对象不变量添加和删除代码契约，但不能为 C# 中的前置条件添加和移除代码契约？

在 CLR via C# 一书中，我遇到了以下摘录：

And since a contract cannot be made stricter with new versions (without breaking compatibility), you should carefully consider preconditions when introducing a new virtual, abstract, or interface member. For postconditions and object invariants, contracts can be added and removed at will as the conditions expressed in the virtual/abstract/interface member and the conditions expressed in the overriding member are just logically AND-ed together.

后置条件和对象不变量、契约可以随意添加和删除，这让我很困惑。我希望有一个建议，即后置条件和对象不变量只能像前置条件一样变得更严格。为什么我期待这个？因为我可以举出一个建议被证明是错误的例子。例如

起初我们有一个后置条件，一切正常：

using System.Diagnostics.Contracts;

public sealed class Program
{
    public static void FooBaseContract(int i) 
    {
        Contract.Ensures(i > 0);
    }
}

public class FooBase 
{
    public virtual int i 
    {
        get {return 2;} 
    }
}
public class FooDerived : FooBase
{
    public override int i 
    {
        get {return 4;} 
    }
}

现在我们决定使后置条件更严格：

using System.Diagnostics.Contracts;

public sealed class Program
{
    public static void FooBaseContract(int i) 
    {
        Contract.Ensures(i > 4);
    }
}

public class FooBase 
{
    public virtual int i 
    {
        get {return 2;} 
    }
}
public class FooDerived : FooBase
{
    public override int i 
    {
        get {return 4;} 
    }
}

这肯定会使使用先前后置条件的代码与新后置条件不兼容。这意味着我们通过使后置条件更严格来失去向后兼容性。

此外，我不明白为什么作者只提到 virtual, abstract, or interface member。因为在我上面给出的人为示例中，即使我将代码更改为以下内容（删除所有 virtual, abstract, or interface member），也会发生与新代码合同版本不兼容的情况：

using System.Diagnostics.Contracts;

public sealed class Program
{
    public static void FooBaseContract(int i) 
    {
        Contract.Ensures(i > 4);
    }
}

public class FooBase 
{
    public int i 
    {
        get {return 2;} 
    }
}

所以，有人可以简单地解释一下我在这里遗漏了什么吗？

更新

如评论部分所述 - 代码契约是一个已弃用的概念。这对我来说没问题，我只是想理解这个想法——在这种情况下，这就是为什么我们可以使后置条件和对象不变量更严格？这与我的常识相矛盾，这意味着之前允许返回某些东西（或发生对象不变量），现在我们声明不再允许返回某些东西，这本书的作者说这种情况并没有打破向后兼容性。

Answer 1

文中说条件"anded"在一起。这意味着您根本没有能力删除后置条件和不变量。不管你怎么写代码，你只能添加它们。

后置条件和不变量是退出时必须确保的事情。能够添加义务是有意义的。如果您要添加矛盾，那么 CC 应该将其标记为违反后置条件。

从兼容性和可扩展性的角度来看，基础 class 的用户将获得他们期望的保证。他们可能会收到他们不知道或不关心的额外保证。

为什么可以为后置条件和对象不变量添加和删除代码契约，但不能为 C# 中的前置条件添加和删除代码契约？

Why code contracts can be added and removed for postconditions and object invariants, but not for preconditions in C#?

c#

code-contracts