1 def recmin(A):
2 if len(A) == 1:
3 return A[0]
4 else:
5 m = len(A) // 2
6 min1 = recmin(A[0..m-1])
7 min2 = recmin(A[m..len(A)-1])
8 return min(min1, min2)
我试图证明这个函数的部分正确性，我想出了一个谓词p(i):for the array A=[0..i]，len(A)=i+1当调用 recmin[A] 时，这个调用终止并返回一些 t ，即0<=t<=i A[t]最小值
但我觉得这个谓词是错误的，我将如何证明后置条件A[0]是最小值