证明程序的正确性答案

【问题标题】：Proving the correctness of a program证明程序的正确性
【发布时间】：2015-11-06 00:48:55
【问题描述】：

函数递归查找并返回具有整数元素的数组中的最小元素

Min(A, b, e)
if (b=e)
     return A[b]
m = (b+e)/2 // floor is taken
x = Min(A, b, m)
y = Min(A, m +1, e)
If(x < y)
     return x
else
     return y

我的前提是：b和e都是大于零的整数

我的后置条件是：返回一个整数 x 或 y（不确定）

那么我如何通过证明前后条件是归纳的来证明这是正确的

对不起格式，新的。

【问题讨论】：

你有按照你的方式编写你的任务吗？分治法在这里没有多大意义，因为无论如何您都必须检查数组元素的每个元素一次，因此可以应用更简单的尾递归方案（如def fun MyMin ( A, idxcur ) = return (idxcur == 0) ? A[idxcur] : min ( MyMin ( A, idxcur-1), A A[idxcur] );）

标签： computer-science proof correctness proof-of-correctness

【解决方案1】：

证明：证明是数学归纳法。

基本情况：考虑 b=e 的情况。我们正在查看大小为 1 的列表 A 的一部分；具有一个元素的列表的最小元素是列表的一个元素，在这种情况下算法返回。

归纳假设：现在假设算法正确地返回了所有大小为 k 且包括 k 的列表的最小元素。证明：它返回最大为 k+1 的列表的最小值。

归纳步骤：我们有 e = b + k + 1 并且想要证明我们返回了最小元素。我们知道 m 将等于 (e+b)/2 = (2b+k+1)/2 = b+(k+1)/2。这会将大小 k+1 的列表分为大小 floor((k+1)/2) 和 cieling((k+1)/2) 两部分。对于所有大于零的 k 值，这两者都小于或等于 k（我们的基本情况从 k=1 开始，所以这意味着我们很好）。因此，根据归纳假设，x 是列表下半部分的最小值，y 是列表上半部分的最小值。如果小于 y，算法返回 x，否则返回 y。由于列表 A 中的最小值必须出现在列表的一半中，并且我们从 A 的两半中返回最小值中的较小者，因此我们知道我们正在返回 A 中的最小值。证明到此结束。

【讨论】：