algorithm - 无等待算法正确性证明的一般方法

Question

我使用通用构造为无等待二叉搜索树设计了一个算法。我有每种方法的线性化点。但我不确定如何正式证明该算法的正确性。

在搜索类似的论文时，我发现他们已经证明了该算法是无等待的并且只生成可线性化的执行。这个条件是必要的还是充分的？

是否有任何其他形式化方法来证明免等待算法的正确性？

Answer 1

要正式证明某事，您需要以下内容:

• 您要证明的事物的准确定义。在您的情况下，这可能是某种始终正确的谓词。我举个例子:

For BlockingQueue capped with size N, the number of elements in the queue should always be [0, N].

If BlockingQueue is empty, the number of times item was added there is equal to number of times it was removed from there.

好的，我们有了定义或/和确切的描述。现在，有几种方法可以证明它:

• 反证法 方法。考虑陈述不正确并最终得出一些不可能的结论。例如，我们要证明Integer numbers can be negative 点。让我声明:

All integer numbers are positive.

这导致我们-1 是一个假的正数，所以这个陈述是不正确的，原来的陈述被证明了。

• 通过使用 Mathematical induction 检查所有情况(对于有限集)来证明对于所有可能的情况，陈述都是正确的(对于 Сountable 集)，或者使用一些更复杂的逻辑语句和方式。更具体的例子取决于我们要证明的定理。

我还要补充一点，根据我的经验，我上面写的Proof by contradiction方法经常被使用，在很多情况下都适用，所以你可能应该先考虑一下。