问题标签 [invariants]

正如在算法简介 ( http://mitpress.mit.edu/algorithms ) 中看到的，练习陈述如下：

输入：数组A[1..n]和一个值v

输出：索引i，在哪里A[i] = v或NIL如果v没有找到A

为 LINEAR-SEARCH 编写伪代码，它扫描序列，寻找 v。使用循环不变量，证明你的算法是正确的。（确保你的循环不变量满足三个必要的属性——初始化、维护、终止。）

我创建算法没有问题，但我没有得到的是如何确定我的循环不变量。我想我理解了循环不变量的概念，即在循环开始之前、每次迭代的结束/开始时始终为真并且在循环结束时仍然为真的条件。这通常是目标，例如，在插入排序、迭代j、从 开始j = 2，A[1..j-1]元素总是被排序的。这对我来说很有意义。但是对于线性搜索？我什么都想不出来，想一个循环不变量听起来太简单了。我理解错了吗？我只能想到一些明显的东西（它不是 NIL 就是介于 0 和 n 之间）。提前非常感谢！

上面的代码是 Java 中的一种方法，用于使用 while 循环计算和返回给定正整数的下对数。我将如何为上面的循环提供不变量？即在它开始之前，每次循环体结束时，以及循环条件的否定都成立。

在契约式设计中，类不变量必须在两种情况下得到满足：创建对象后和调用例程后。是否有任何示例或条件，我也必须在调用例程之前进行评估？

我已经听到/阅读了很多关于 C# 中的协方差问题的内容，我想提出一些问题和场景，希望我能澄清我对此事的困惑。

在这些示例中，请假设始终定义以下内容：

我的第一个例子：

这应该有效，对吗？我在 C# 中对此进行了几次测试，它编译得很好并且运行良好（我对第一个示例的测试比这略多，因为我有将内容打印到控制台的多态调用）。

第二个例子：

在第二个示例中，我的理解是这不应该编译，并且是 .NET 4.0 中解决的协方差问题的根源。如果我错了，请纠正我。我也知道.NET 4.0 不允许具体类型之间的协变/逆变，只有接口。

最后，我想得到一些定义。我不太清楚这三个术语背后的含义：

• 协方差
• 逆变
• 不变性（与不变性相同？）

至于最后一个词，我在 C++ 中经常使用它来指代隐含规则的更改。例如，如果我有一个整数并且它只允许有 1 到 10 之间的值，那么“不变性”就是它只能在 1 到 10 之间。我可能会误解这一点，我也不确定是否对于此特定讨论，此定义很好地转换为 C#。

编辑

我的目标是准确了解 C# 中泛型接口的协方差或转换问题。我发布的示例是我对问题所在的理解。如果所有示例都编译/运行良好，请提供一个示例，该示例确实重现了 C# 中最常见的协变/逆变/转换问题。我需要知道这一点，以便我可以识别并向其他人解释问题。

很简单，在设计一个新类时，我如何确定不变量应该是什么？什么定义了不变量？我听说它与有效性有关，但这仍然模棱两可。使给定实例有效或无效的原因是有争议的。

我应该只凭我的“直觉”感觉吗？是否有确定不变量是什么的指导方针？

对不起，如果这个问题似乎太长了。在我问它之前，我需要说明它来自哪里。

设置：

给定以下不可变类型Rectangle：

…从中派生一个类型似乎是完全合法的Square：

…因为派生类可以确保它自己的不变量永远不会被违反。

但是一旦我变得Rectangle可变：

......我不应该再从中派生Square，因为Square不应该有独立的设置器Widthand Height。

问题：

我可以用代码合同做什么，以便一旦我Square从可变Rectangle类派生它就会警告我违反合同？最好，Code Contracts 的静态分析已经在编译时给了我一个警告。

换句话说，我的目标是使用代码合同对以下规则进行编码：

• Width和HeightaRectangle可以相互独立地改变。
• Width和HeightaSquare不能相互独立地改变，这首先是没有意义的。

......并以这样一种方式进行，即每当这些规则“冲突”时，代码合同都会注意到。

到目前为止我所考虑的：

1. 添加一个不变量Rectangle：

这种方法的问题在于，虽然不变量正确地说明了“宽度和高度不必相等，但它们可以相等”，但它是无效的，（1）因为它是重言式，（2）因为它比Width == Height派生类中的不变量限制更少Square。也许它甚至在代码契约看到它之前就被编译器优化掉了。

2. 给Rectanglesetter 添加后置条件：

这将禁止派生类简单Square地更新Height为Width无论何时Width更改，反之亦然，它本身Square不会阻止我从Rectangle. 但这就是我的目标：让代码合同警告我Square不能从可变的Rectangle.

C++ 中有没有办法强制在类中使用 getter 或 setter？

我唯一想到的是将所有超级私有成员作为私有变量放入具有受保护的 getter/setter 的抽象基类中。

但这听起来不是好的做法。

有没有更常见的方法或约定来确保每个人都使用设置器？

（我的目的：如果类变得更大，我发现很难记住哪些变量带有不变量。目前在设置我搜索的任何变量之前，我是否创建了一个 getter 或 setter（以确定我是否必须考虑不变量）。但我想每次都摆脱这种不专业的搜索。）

您好我有几个关于领域驱动设计和使用工厂/工厂方法的问题。根据域驱动设计蓝皮书（Eric EVan's Book），它指出复杂的构造函数应该封装在工厂/工厂方法/构建器中，因此有一个一致的地方可以检查所有不变量，所以我的问题是关于这个：

假设我正在开发一个魔术管理器应用程序，您可以在其中对魔术效果进行类似 CRUD 的操作（例如博客上的帖子 + 效果持续时间、使用的材料（字符串列表）、与魔术效果相关的模式等多个属性）和一些不变量中的一个是魔术效果必须始终具有标题、魔术效果的内容、持续时间和可选模式，并且必须由在应用程序中注册的用户发布。

因此，由于我有很多不变量，所以我有一个 EffectBuilder 来构建 MagicEffect 对象并检查所有不变量。

在用户类中做这样的事情可以吗？

或者我应该做类似的事情：

还有别的地方

我的意思是第一个示例我有一个带有大量参数的巨大方法，但我确保在构建它时将所有不变量都设置在效果中，在另一种情况下，我通过具有流畅的界面以编程方式提高代码可读性，但我无法制作确保 100% 的时间满足不变量。

哪种方法更好？有没有更平衡的方法呢？

谢谢巴勃罗

What is the Loop Invariant(s) in this sample code.
This is an excerpt code implemented in C programming language:

These are my initial answers (Loop Invariant):

1. y>=n
2. x<=m
3. z>=0

I am still unsure about this. Thanks.

有没有人有关于如何/什么是在 C# 中实现 Stack 类的最佳方法的任何示例或想法？我知道已经有一个 Stack 类，但我需要了解如何实际实现一个 Stack 类。

我还需要有关如何在 C# 中使用 Contracts 为此类指定前置条件、后置条件和不变量的建议。我想我之前在 ASP.NET MVC 架构中创建模型时使用过类似的东西，但我不完全确定它是否是相同的东西并且以相同的方式工作。（如果你还不能告诉我，我对先决条件/后置条件/不变量有点迷茫 - 所以请多多包涵。）

我的主要问题- 有人可以给我关于正确使用合同的建议，例如堆栈。

是的，我已经付出了努力：