如何證明以下算法的正確性？

考慮以下算法min，它將列表x，y作爲參數，並以x和y的並集返回第z個最小元素。前提條件：X和Y是按升序排列的整數列表，它們是不相交的。如何證明以下算法的正確性？

公告稱，其僞代碼，所以索引從1開始不是0

Min(x,y,z): 
    if z = 1: 
     return(min(x[1]; y[1])) 
    if z = 2: 
     if x[1] < y[1]: 
      return(min(x[2],y[1])) 
     else: 
      return(min(x[1], y[2])) 

q = Ceiling(z/2) //round up z/2 

if x[q] < y[z-q + 1]: 
    return(Min(x[q:z], y[1:(z - q + 1)], (z-q +1))) 
else: 
    return(Min(x[1:q], B[(z -q + 1):z], q))

我可以證明它終止，因爲Z保持2下降，最終將達到的基本情形之一的，但我不能證明部分正確性。

來源

2013-03-21 user65065

嗨，我認爲這對計算機科學來說更合適嗎？ – user65065 2013-03-21 22:44:13

你能更詳細地指定算法應該做什麼嗎？我明白你想要'x'和'y'的元素中的第k個最小元素，即'Mix（[1,2]，[3,4]，1）= 1'（最小元素） 'Mix（[1,2]，[3,4]，2）= 2'（第二小元素）等等。是嗎？如果是這樣，我不認爲上述算法是正確的。甚至沒有任何遞歸。 – chris 2013-03-23 03:58:49

當然，如果沒有遞歸，終止是微不足道的。如果你有遞歸，你的論點不能保證終止（假設你的意思是整數，而不是自然數），因爲減少一個負整數可以繼續（理論上）永遠不會觸及基本情況。 – chris 2013-03-23 04:07:49

您的代碼不正確。

考慮以下輸入：

x = [0,1] 
y = [2] 
z = 3

你再q = 2，並且在if條款後面，訪問y[z-q+1]，即y[2]英寸這是一個數組邊界違規。

來源

2013-05-01 13:51:51

如何證明以下算法的正確性？

回答

相關問題