雖然不知道大牛怎麼想到這樣解決補碼的正負表示問題1，但這種解決辦法的正確性倒是可以嘗試證明一下。
首先需要明確什麼叫正確性，充要條件暫時沒有想到，先列舉幾個必要條件，至少這些條件需要能成立：
本身的值表示正確
本身的符號表示正確
運算結果的值表示正確
運算結果的符號表示正確
接下來證明每乙個條件：
一定正確，左邊加一位對值來說是完全不影響的，可以從兩個角度分析
左邊加1就等於加了乙個模
左邊是高位，本身的運算只會向高位進製，完全不會影響低位的運算
只要用這個符號系統表示，就會自然正確
沒想到好辦法，只能分情況討論。
1）值的位運算不溢位
兩個正數符號一致
數學結果：兩個正數相加還是正數，符號一定為正
位運算結果：因為值的位運算不溢位，兩個0相加還是0，也就是正
兩個負數情況不存在
數學結果：符號一定為負
位運算結果：值的位運算不溢位，兩個1相加進一位得到0，也就是正
看起來兩個結果的符號一定不一致。但其實可以證明這種「值的位運算不溢位」情況下「數**算結果一定溢位」，而數**算結果溢位的情況不用考慮，我們不保證這種情況下運算結果的正確性
證明：
假設負數a的補碼表示是[1
a1a2
a3] ，它的數學大小 =−
8+(a
1∗22
+a2∗
2+a3
) ，設右側為
a ，那麼數學大小 =−
8+a 假設負數b的補碼表示是[1
b1b2
b3] ，它的數學大小 =−
8+(b
1∗22
+b2∗
2+b3
) ，設右側為
b ，那麼數學大小 =−
8+b 那麼「值的位運算不溢位」這個條件用數學表示就是 a+
b<
8 這時候計算數**算結果：−8
+a−8
+b=−
16+a+
b ，因為a+
b<
8 ，所以這個結果一定小於−8
，而它的表示範圍是−8
7 ，所以溢位了
一正一負
正數絕對值大於負數情況不存在
數學結果：正
位運算結果：0和1相加得到1，也就是負
雖然結果不一致，但是可以證明這種情況不存在，也就是「正數絕對值大於負數」時「值的位運算一定溢位」
證明：
假設正數a的補碼表示是[0
a1a2
a3] ，它的數學大小 =a
1∗22
+a2∗
2+a3
=a假設負數b的補碼表示是[1
b1b2
b3] ，它的數學大小 =−
8+(b
1∗22
+b2∗
2+b3
)=−8
+b「正數絕對值大於負數」的數學表示是 a−
8+b>0⇒
a+b>
8 「值的位運算」結果為a+
b ，它一定大於8就說明溢位了
正數絕對值小於負數符號一致
數學結果：負
位運算結果：0和1相加得到1，也就是負
正數絕對值等於負數情況不存在
位運算結果需要是0，而如果值位不溢位，符號一定為負，其實通過「正數絕對值大於負數」這個證明可能看出，正數絕對值等於負數時值位也一定溢位
2）值的位運算溢位
兩個正數情況不存在
兩個正數的值位運算溢位意味著運算結果大於8，意味著數**算結果溢位，不考慮
兩個負數符號一致
數學結果：一定是負的
位運算結果：兩個1相加是0，但是有進製，如果進製為1就沒問題，那進製會不會是2呢？不會，因為後三位最大是7，兩個7是14，不超過16，所以結果也是負數
一正一負
正數絕對值大於等於負數符號一致
數學結果：正
位運算結果：0和1相加得到1，溢位1位得到0，也就是正
正數絕對值小於負數情況不存在
數學結果：負
位運算結果同上，為正
但這種情況不存在，也就是「正數絕對值小於負數」一定不「值的位運算溢位」
證明 假設正數a的補碼表示是[0
a1a2
a3] ，它的數學大小 =a
1∗22
+a2∗
2+a3
=a假設負數b的補碼表示是[1
b1b2
b3] ，它的數學大小 =−
8+(b
1∗22
+b2∗
2+b3
)=−8
+b「正數絕對值小於負數」數學表示是 a−
8+b<0⇒
a+b<
8 ，說明值的位運算一定不溢位
總結以上對於「運算結果的符號表示正確」的證明，所有存在的情況中，符號都是一致的，所以運算結果的符號表示也是正確的。
綜上所述，4個條件均成立，所以從目前來看，補碼的正確性是可以保證的。
見計算機中整數為什麼以「補碼」的形式儲存？
↩
krusal演算法正確性的證明
krusal演算法步驟如下 新建圖g，g中擁有原圖中相同的節點，但沒有邊 將原圖中所有的邊按權值從小到大排序 從權值最小的邊開始，如果這條邊連線的兩個節點於圖g中不在同乙個連通分量中，則新增這條邊到圖g中 重複3，直至圖g中所有的節點都在同乙個連通分量中 為什麼這一定是最小生成樹呢？關鍵還是步驟3中...
kmp優化正確性證明
鄧俊輝老師的課上給出了一種普遍的kmp演算法優化，但是沒有給出這種優化的正確性證明。或許這種正確性是顯而易見的，但這裡還是研究了一下這個演算法的正確性問題。int buildnext char p else 原演算法 j next j 優化演算法 j newnext j return next 顯然...
Dijkstra演算法正確性證明
問題 求圖中點1到其他各點的最短距離 演算法描述 設初始時圖的所有點的集合u 把起點s放入初始集合set中 u u set set 找s經過集合set中的點，能達到的距離最短的點k k in u 將k併入set 言外之意k的前乙個點必然屬於set u u set set 由於每次引入的只有乙個點k，...