proof-of-correctness

4熱度

3回答

我是新來的輔酶Q，我試圖證明這一點...... Theorem andb_eq_orb : forall (b c : bool), (andb b c = orb b c) -> (b = c). 這是我的證明，但我碰到困難時，我得到的目標（假=真 - >假=真）。 Proof. intros b c. induction c. destruct b. refle

0熱度

1回答

證明正確的，並征服排序

假設我們有一個排序方法： void DD_sort(int a[], int x, int y, int size_a) { if(x == y){ return; } else if(y == x+1){ if(a[x] > a[y]){ /* swap the content */ return; }

0熱度

1回答

循環不變Hoare邏輯

我有一個程序，我應該找到一個循環不變量，然後提供一個證明。 {x>=0 && y>=0} // precondition res:=0; i:=0; while (i<y) do res:=res+x; i:=i+1; od {res:=x*y} //postcondition 唯一合乎邏輯的循環不變對我來說是res<=x*y，這是後置條件簡單，但我不認爲它最好的一個

1熱度

1回答

後綴樹根邊緣的證明

我想知道如何編寫一個證據，證明後綴樹中分支或根邊的數量等於字符串S的字母大小。假設我們有S = {aaabaac} ，字母表= {a，b，c}，字母大小= 3，那麼根邊緣（或從根開始的分支）僅僅是3，即a，b和c。或者這可以通過定義來證明嗎？我不確定！

2熱度

1回答

驗證程序的等價性

優化編譯器的最終目的是在程序空間中搜索等價於原始程序但速度更快的程序。這已經在實踐中用於非常小的基本塊：https://en.wikipedia.org/wiki/Superoptimization 聽起來很難的部分是搜索空間的指數性質，但實際上它不是;最難的部分是，假設你找到了你想找的東西，你如何證明這個新的，更快的程序與原始程序真的是相同的？上次我研究過它，在某些情況下證明程序的某些屬性已經

0熱度

1回答

證明程序的正確性

功能遞歸地查找並從具有整數元素 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爲大於零的整數

0熱度

1回答

葡萄酒貿易貪婪解決方案（SPOJ）的正確性證明？

不要誤會我在網上法官上發佈問題的問題。我只想知道如何證明解決方案的正確性。以下是Wine trading problem的問題。它說，在單位距離有一排房子，每個房子要麼出售或購買葡萄酒。總需求=總供給。在交易中完成的工作是涉及距離的葡萄酒數量。問題是滿足所有房屋在最低限度工作中的需求。所提出的解決方案是，第一個賣方（比如從右側開始）賣給第一個買方（金額= min（賣方，買方））（這是貪婪的選擇），

0熱度

1回答

Bellman-Ford算法的正確性證明

我正試圖學習Bellman-Ford算法，但我被證明正確性困擾。我已經使用Wikipedia，但我根本無法理解證明。我在Youtube上找不到任何有用的東西。希望你們任何人都能簡單解釋一下。此頁"Bellman-ford correctness can we do better"不回答我的問題。謝謝。

2熱度

2回答

在伊德里斯，我如何從一個類型中提取證據？

如果我有一個So的類型，比如So (x < y)，通過創造的東西像 IsLt : Ord a => (x: a) -> (y: a) -> Type IsLt x y = So (x < y) 我怎樣才能提取(x < y)證明了這件事？我無法在標準庫中找到此功能。 So在標準庫中定義爲： data So : Bool -> Type where Oh : So True 而且我

-1熱度

1回答

什麼編程語言具有測試併發算法的具體目的？

我的一位同事編寫了一個程序，證明在測試運行多個併發線程的算法試圖找到可能觸發不需要的條件的序列之後，某些條件將不會被滿足。他使用了專爲此目的而設計的計算機語言，但我不記得它的名字。爲此特定目的提供哪些語言？