问题标签 [invariants]

我一直在考虑创建一个 Java 框架，允许程序员在接口上指定不变量（前置条件和后置条件）。目的是使代码更加健壮并减少需要为同一接口的不同实现编写的单元测试的数量。

我设想创建某种方法，用程序员也会编写的不变量来注释方法。例如

将用注释装饰，以确保任何实现都返回排序列表。此注释将链接到可以在编译时针对任何实现运行的单元测试。

这是一个疯狂的想法还是对更广泛的编程社区有用？

我正在开发一个 Android 应用程序。

我想将大小设置为这样的 char 数组：

但它不起作用。我必须删除第五个才能使其正常工作。

我想将语言变量限制为五个字符。我怎样才能做到这一点？

谢谢。

我有一个 JML 问题。有什么区别

并将其声明为

关于array_的元素？在每种情况下，他们拥有什么属性？

提前致谢。

在coders at work中，作者问“如何在代码中使用不变量”。请解释这个问题是什么意思。

我在 wiki 上看到了类不变量，但这个例子是用 Java 编写的，我在 Java 方面的熟练程度不足以将这个例子与 C# 联系起来。.NET 4.0 引入了不变性、协变和逆变，并在此处进行了很好的解释。不变性是如此广泛。作者对该词的使用似乎与单元测试有关。对于读过这本书的人来说，作者是什么意思？我们是在谈论做出假设并在单元测试之后简单地测试有效性吗？

有人可以为我提供简单的 C# 示例，例如协变、逆变、不变性和逆变性（如果存在这种情况）。

到目前为止，我看到的所有样本都只是将一些对象投射到System.Object.

是否有任何已建立的模式来检查 C++ 中的类不变量？

理想情况下，将在每个公共成员函数的开始和结束时自动检查不变量。据我所知，带有类的 C 语言提供了特殊before的after成员函数，但不幸的是，当时契约式设计并不是很流行，除了 Bjarne 之外没有人使用该功能，因此他将其删除。

当然，check_invariants()在每个公共成员函数的开头和结尾手动插入调用既繁琐又容易出错。由于 RAII 是处理异常的首选武器，因此我提出了以下方案，将不变性检查器定义为第一个局部变量，并且该不变性检查器在构造和销毁时检查不变量：

问题#0：我想没有办法声明一个未命名的局部变量？:)

我们仍然必须check_invariants()在构造函数的末尾和析构函数Foo的开头手动调用。Foo但是，许多构造函数体和析构函数体是空的。在那种情况下，我们可以使用 aninvariants_checker作为最后一个成员吗？

问题 #1：即使对象仍在构造中，传递this给invariants_checker立即通过该指针调用的构造函数是否有效？check_invariantsFoo

问题 #2：您认为这种方法还有其他问题吗？你能改进它吗？

问题 3：这种方法是新的还是众所周知的？有没有更好的解决方案？

我正在查看 Hoare Logic，但在理解查找循环不变量的方法时遇到了问题。

有人可以解释用于计算循环不变量的方法吗？

循环不变量应该包含什么才能成为“有用的”？

我只处理简单的示例，在以下示例中查找不变量并证明部分和完全更正：

考虑以下

这将允许创建

也是“非法”

“非法”，因为元数与参数列表的长度不匹配。

缺少使用这样的功能

并且只从 Predicate 模块导出 makePred ，有没有办法强制值构造函数的正确性？

我正在为我的考试修改算法，我试图解决这个练习，但我想不出一个解决方案。

这是伪代码。

因此，现在的代码不满足后置条件，因为对于某些输入（例如 x = 1 和 a={0,1,1,1,1}），第 14 行返回的值不满足第 4 行的后置条件。练习要求：“替换第 14 行的“return middle;”。通过 while 循环并返回代码，使其满足后置条件。包括足够强的变体和不变式以暗示返回时的后置条件. 提示：确保你包括说明没有改变的内容。

我一直无法找到解决方案。谁能帮我？

提前谢谢，VJ

编辑：好的，谢谢你们俩的帮助。

} 返回中间；

我选择了中间的变体。并且不变量是：

0x

你认为这是正确的吗？

如果我的类不变量无效，我想抛出运行时异常。由于这是一个编程错误（类似于 NullPointerException），客户端不应捕获该异常。

异常类应该声明为私有的还是公共的（或其他）？

是否有关于自定义运行时异常和可见性的指南？