logic - 是不变量，重言式吗？

Question

所以我在阅读 Assertions Java API 时遇到了术语不变量。在我阅读了网上的其他文章后，我理解不变量是重言式。我误会了吗？

Answer 1

考虑一下程序应该做什么和它实际做什么之间的区别。如果程序正确，则所有断言都是重言式。如果程序有问题，他们不会。

Answer 2

在逻辑上，重言式是根据自己的定义为真的陈述，因此从根本上说是没有信息的。逻辑重言式在论点或陈述中使用循环推理。

不变量只是不会改变的东西。

Answer 3

重言式是永远正确的陈述。不变量是旨在在特定上下文中为真的陈述。

一些不变量不是重言式。例如，在i每次迭代加 1 并在 时终止的编程循环中i=max，您可以i < max在循环顶部声明一个不变量。这不是重言式，因为条件并非普遍正确：i小于没有逻辑必然性max。其目的是每次在特定计算的上下文中达到特定点时都是真的。