为了证明快速排序总是终止，您首先要证明它在长度为 1 的输入时终止。（这确实是正确的。）然后证明如果它在长度达到 n 的输入时终止，那么它将终止长度为 n+1 的输入。由于归纳，这足以证明算法对于所有输入都会终止。
要证明快速排序是正确的，必须将比较排序的规范转换为精确的数学语言。我们希望输出是输入的排列，这样如果i ≤ j 则 ai ≤ aj。证明快速排序的输出是输入的排列很容易，因为它从输入开始并且只是交换元素。证明第二个属性有点棘手，但您可以再次使用归纳法。
To prove the correctness of an algorithm, you typically have to show (a) that it terminates and (b) that its output satisfies the specification of what you're trying to do. These two proofs will be rather different from the algebraic proofs you mention in your question. The key concept you need is mathematical induction. (It's recursion for proofs.)
To prove that quicksort always terminates, you would first show that it terminates for input of length 1. (This is trivially true.) Then show that if it terminates for input of length up to n, then it will terminate for input of length n+1. Thanks to induction, this is sufficient to prove that the algorithm terminates for all input.
To prove that quicksort is correct, you must convert the specification of comparison sorting to precise mathematical language. We want the output to be a permutation of the input such that if i ≤ j then ai ≤ aj. Proving that the output of quicksort is a permutation of the input is easy, since it starts with the input and just swaps elements. Proving the second property is a little trickier, but again you can use induction.
You don't give many details but there is a community of mathematicians (Mathematical Knowledge Management MKM) who have developed tools to support computer proofs of mathematics. See, for example:
Where i am stuck is proving prims and Kruskals - how can i get these algorithms in to a form like the mathmatical one above so i can proceed to prove
I don't think you can directly. Instead, prove that both generate a MST, then prove that any two MST are equal ( or equivalent, since you can have more than one MST for some graphs ). If both algorithms generate MSTs which are shown to be equivalent, then the algorithms are equivalent.
From my maths classes at Uni I (vaguely) remember proving Prims and Kruskals algorithms - and you don't attack it by writing it in a mathematical form. Instead, you take proven theories for Graphs and combine them e.g. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness to build the proof.
If your looking to prove the complexity, then simply by the working of the algorithm it's O(n^2). There are some optimisations for the special case where the graph is sparse which can reduce this to O(nlogn).
Most of the times the proof depends on the problem you have in your hand. Simple argument can be suffice at times, at some other times you might need rigorous proof. I once used a corollary and proof of already proved theorem to justify my algorithm is right. But that is for a college project.
Maybe you want to try out a semi-automatic proof method. Just to go for something different ;) For example, if you have a Java specification of Prim's and Kruskal's algorithms, optimally building upon the same graph model, you can use the KeY Prover to prove the equivalence of the algorithm.
The crucial part is to formalize your proof obligation in Dynamic Logic (this is an extension of first-order logic with types and means of symbolic execution of Java programs). The formula to prove could match the following (sketchy) pattern:
\forall Graph g. \exists Tree t.
(<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t)
This expresses that for all graphs, both algorithms terminate and the result is the same tree.
If you're lucky and your formula (and algorithm implementations) are right, then KeY can prove it automatically for you. If not, you might need to instantiate some quantified variables which makes it necessary to inspect the previous proof tree.
After having proven the thing with KeY, you can either be happy about having learned something or try to reconstruct a manual proof from the KeY proof - this can be a tedious task since KeY knows a lot of rules specific to Java which are not easy to comprehend. However, maybe you can do something like extracting an Herbrand disjunction from the terms that KeY used to instantiate existential quantifiers at the right-hand side of sequents in the proof.
Well, I think that KeY is an interesting tool and more people should get used to prove critical Java code using tools like that ;)
发布评论
评论（6）
为了证明算法的正确性，您通常必须证明 (a) 它终止，并且 (b) 它的输出满足您想要执行的操作的规范。这两个证明与您在问题中提到的代数证明有很大不同。您需要的关键概念是数学归纳法。 （这是证明的递归。）
让我们采用quicksort 为例。
为了证明快速排序总是终止，您首先要证明它在长度为 1 的输入时终止。（这确实是正确的。）然后证明如果它在长度达到 n 的输入时终止，那么它将终止长度为 n+1 的输入。由于归纳，这足以证明算法对于所有输入都会终止。
要证明快速排序是正确的，必须将比较排序的规范转换为精确的数学语言。我们希望输出是输入的排列，这样如果i ≤ j 则 ai ≤ aj。证明快速排序的输出是输入的排列很容易，因为它从输入开始并且只是交换元素。证明第二个属性有点棘手，但您可以再次使用归纳法。
To prove the correctness of an algorithm, you typically have to show (a) that it terminates and (b) that its output satisfies the specification of what you're trying to do. These two proofs will be rather different from the algebraic proofs you mention in your question. The key concept you need is mathematical induction. (It's recursion for proofs.)
Let's take quicksort as an example.
To prove that quicksort always terminates, you would first show that it terminates for input of length 1. (This is trivially true.) Then show that if it terminates for input of length up to n, then it will terminate for input of length n+1. Thanks to induction, this is sufficient to prove that the algorithm terminates for all input.
To prove that quicksort is correct, you must convert the specification of comparison sorting to precise mathematical language. We want the output to be a permutation of the input such that if i ≤ j then ai ≤ aj. Proving that the output of quicksort is a permutation of the input is easy, since it starts with the input and just swaps elements. Proving the second property is a little trickier, but again you can use induction.
您没有提供太多细节，但有一个数学家社区（数学知识管理 MKM）开发了支持计算机数学证明的工具。例如，请参阅：
http://imps.mcmaster.ca/
和最新会议
http://www.orcca.on.ca/conferences/cicm09/mkm09/
You don't give many details but there is a community of mathematicians (Mathematical Knowledge Management MKM) who have developed tools to support computer proofs of mathematics. See, for example:
http://imps.mcmaster.ca/
and the latest conference
http://www.orcca.on.ca/conferences/cicm09/mkm09/
我认为你不能直接证明。相反，证明两者都生成一个 MST，然后证明任何两个 MST 相等（或等效，因为对于某些图可以有多个 MST）。如果两种算法生成的 MST 被证明是等效的，则这些算法是等效的。
I don't think you can directly. Instead, prove that both generate a MST, then prove that any two MST are equal ( or equivalent, since you can have more than one MST for some graphs ). If both algorithms generate MSTs which are shown to be equivalent, then the algorithms are equivalent.
从我在大学的数学课上，我（模糊地）记得证明 Prims 和 Kruskals 算法 - 并且你不会通过以数学形式编写它来攻击它。相反，您采用经过验证的图理论并将它们结合起来，例如 http://en.wikipedia。 org/wiki/Prim%27s_algorithm#Proof_of_ Correctness 来构建证明。
如果您想证明复杂性，那么简单地通过算法的工作原理，它就是 O(n^2)。对于图稀疏的特殊情况有一些优化，可以将其减少到 O(nlogn)。
From my maths classes at Uni I (vaguely) remember proving Prims and Kruskals algorithms - and you don't attack it by writing it in a mathematical form. Instead, you take proven theories for Graphs and combine them e.g. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness to build the proof.
If your looking to prove the complexity, then simply by the working of the algorithm it's O(n^2). There are some optimisations for the special case where the graph is sparse which can reduce this to O(nlogn).
大多数时候，证明取决于你手上的问题。有时简单的论证就足够了，但有时您可能需要严格的证明。我曾经使用已经证明的定理的推论和证明来证明我的算法是正确的。但这是针对大学项目的。
Most of the times the proof depends on the problem you have in your hand. Simple argument can be suffice at times, at some other times you might need rigorous proof. I once used a corollary and proof of already proved theorem to justify my algorithm is right. But that is for a college project.
也许您想尝试一种半自动证明方法。只是为了寻求不同的东西;) 例如，如果您有 Prim 和 Kruskal 算法的 Java 规范，并且最佳地构建在相同的图形模型上，则可以使用 Key Prover 证明算法的等价性。
关键部分是在动态逻辑中形式化你的证明义务（这是一阶逻辑的扩展，具有 Java 程序符号执行的类型和方法）。要证明的公式可以匹配以下（粗略）模式：
这表示对于所有图，两种算法都会终止并且结果是同一棵树。
如果您很幸运并且您的公式（和算法实现）是正确的，那么 KeY 可以自动为您证明。如果没有，您可能需要实例化一些量化变量，这使得有必要检查先前的证明树。
在用 KeY 证明了这一点之后，您可以为学到一些东西而感到高兴，也可以尝试根据 KeY 证明重建手动证明 - 这可能是一项乏味的任务，因为 KeY 知道许多特定于 Java 的规则，而这些规则不容易理解理解。然而，也许你可以做一些事情，比如从 KeY 用于在证明中序列右侧实例化存在量词的术语中提取 Herbrand 析取。
嗯，我认为 KeY 是一个有趣的工具，更多的人应该习惯使用这样的工具来证明关键的 Java 代码；）
Maybe you want to try out a semi-automatic proof method. Just to go for something different ;) For example, if you have a Java specification of Prim's and Kruskal's algorithms, optimally building upon the same graph model, you can use the KeY Prover to prove the equivalence of the algorithm.
The crucial part is to formalize your proof obligation in Dynamic Logic (this is an extension of first-order logic with types and means of symbolic execution of Java programs). The formula to prove could match the following (sketchy) pattern:
This expresses that for all graphs, both algorithms terminate and the result is the same tree.
If you're lucky and your formula (and algorithm implementations) are right, then KeY can prove it automatically for you. If not, you might need to instantiate some quantified variables which makes it necessary to inspect the previous proof tree.
After having proven the thing with KeY, you can either be happy about having learned something or try to reconstruct a manual proof from the KeY proof - this can be a tedious task since KeY knows a lot of rules specific to Java which are not easy to comprehend. However, maybe you can do something like extracting an Herbrand disjunction from the terms that KeY used to instantiate existential quantifiers at the right-hand side of sequents in the proof.
Well, I think that KeY is an interesting tool and more people should get used to prove critical Java code using tools like that ;)