java - 理论上是否可以使用静态分析工具证明Java代码不存在竞争条件？

Question

已关闭。这个问题是 off-topic 。目前不接受答案。

---

想要改进这个问题吗？ Update the question所以它是on-topic用于堆栈溢出。

已关闭11 年前。

Improve this question

无论市场上有哪些静态分析工具，理论上是否有可能使用静态分析工具证明 Java(或任何其他命令式语言)代码不存在竞争条件？

Answer 1

“Java 代码没有竞争条件”这一说法相当模糊。也许您指的是其中之一:

• 静态分析工具能否证明 Java 程序不存在竞争条件？显然不是，因为确实存在具有竞争条件的 Java 程序。

• 静态分析工具总能证明无竞争条件的Java程序没有竞争条件吗？不，因为这相当于解决停止问题(在可能终止也可能不会终止的循环后面放置一个静态竞争条件。要判断竞争是否真的会发生，您需要知道循环是否终止)。

• 静态分析工具有时能否证明无竞争条件的Java程序没有竞争条件？是的。事实上，这样的工具可能非常有用。