arrays - 需要帮助证明循环不变性(简单的冒泡排序,部分正确性)

标签 arrays algorithm sorting loop-invariant proof-of-correctness

冒泡排序算法(伪代码):

Input: Array A[1...n]
for i <- n,...,2 do
    for j <- 2,...,i do
        if A[j - 1] >= A[j] then
            swap the values of A[j-1] and A[j];

我不确定,但我的证明似乎有效,但过于复杂。你能帮我清理一下吗?

Loop-invariant: After each iteration i, the i - n + 1 greatest elements of A are in the position they would be were A sorted non-descendingly. In the case that array A contains more than one maximal value, let the greatest element be the one with the smallest index of all the possible maximal values.

Induction-basis (i = n): The inner loop iterates over every element of A. Eventually, j points to the greatest element. This value will be swapped until it reaches position i = n, which is the highest position in array A and hence the final position for the greatest element of A.

Induction-step: (i = m -> i = m - 1 for all m > 3): The inner loop iterates over every element of A. Eventually, j points to the greatest element of the ones not yet sorted. This value will be swapped until it reaches position i = m - 1, which is the highest position of the positions not-yet-sorted in array A and hence the final position for the greatest not-yet-sorted element of A.

After the algorithm was fully executed, the remaining element at position 1 is also in its final position because were it not, the element to its right side would not be in its final position, which is a contradiction. Q.E.D.

最佳答案

我倾向于用以下术语重写你的证明: 冒泡排序 A[1..n]: 对于我在 n..2 对于 2..i 中的 j 交换 A[j - 1], A[j] 如果它们还没有按顺序排列

循环不变量: 让 P(i) <=> 对于所有 k s.t.我 < k <= n。 A[k] = max(A[1..k])

基本情况: 最初 i = n 并且不变量 P(n) 被平凡地满足。

归纳步骤: 假设不变量对某些 P(m + 1) 成立, 表明在内循环执行后,不变量对 P(m) 成立。

关于arrays - 需要帮助证明循环不变性(简单的冒泡排序,部分正确性),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/51256511/

相关文章:

C++。我试图通过在开关中使用数组来获取用户输入,但是当我运行代码时它显示段错误?

java - 从 JAVA + StackOverflowError 中的集合项生成唯一对

javascript - 使用 Highchart 树状图(向下钻取)

python-3.x - 在数字范围内对列表进行排序

c++ - 如何在 C++ 中对长 vector 使用 std::sort()?

performance - 预处理一组常量字符串以进行二进制搜索

c++ - 在 C++ 构造函数中为结构数组分配存储空间

php - 使用数组更新数据库

string - 打印字符串的所有排列且不重复的算法

javascript - 在 JavaScript 中搜索数组中的子数组