hoare-logic

    2熱度

    1回答

    在形式邏輯中證明正確性

    我想知道是否有人能幫我回答這個問題。它來自之前的考試報告，我可以在知道準備好今年考試的答案的情況下做。 這個問題似乎很簡單，我完全失去了，究竟是什麼要求？ 考慮代碼涉及整數變量的以下部分： if (i < j) { m = i; } else { m = j; } 通過規定適當的輸出條件，然後驗證 正確性的代碼段的，證明執行之後，m是等於 i和j的最小值。 我已經拿到了
    proof formal-methods post-conditions hoare-logic proof-of-correctness 2012-05-24

    0熱度

    1回答

    霍爾邏輯，計算預條件

    if x < 15: x = x+1 else: x = 0 柱條件是：Q = {0 < = X < = 15} 是正確的預條件P1 = { - 1 < = X}或P2 = { 0 < = x < = 15} 而我該如何計算它？
    condition preconditions hoare-logic 2017-08-02

    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，這是後置條件簡單，但我不認爲它最好的一個
    proof-of-correctness hoare-logic 2015-07-19

    0熱度

    1回答

    霍爾邏輯證明

    請證明以下內容是正確的。 {n != 0} if n<0 then n= -n {n>0} 以下推理規則應該幫助 {B and P} S {Q}, (not B) and P=>Q --------------------------------- {P}if B then S{Q} 我一直在尋找所有網站上有一個明確的解釋，或者至少一個例子來跟着，但我不太明白，我發現了一些可能
    proof language-concepts hoare-logic 2014-10-01

    0熱度

    1回答

    Hoare分區陷入無限循環

    我想寫一個採用數組作爲輸入的Hoare分區函數，並將它與第一個元素一起分區（我知道這不是一個好主意，我應該使用隨機化樞軸，像median-of-medians方法）。問題是這個函數在第一個元素最高時落入無限循環，如同數組[14,6,8,1,4,9,2,1,7,10,5]。在外層while的第一次迭代之後，我可以看到這個錯誤，i和j都等於10，因此循環將一直持續。我應該修補哪一部分以獲得理想的效果？
    python partitioning quicksort hoare-logic 2012-09-20

    3熱度

    1回答

    什麼是循環不變和最弱的前提

    給出一個循環不變，維基百科的名單，一個很好的方式，產生一個循環 最弱的先決條件（從http://en.wikipedia.org/wiki/Predicate_transformer_semantics）之間的關係： wp(while E inv I do S, R) = I \wedge \forall y. ((E \wedge I) \implies wp(S,I \we
    formal-methods formal-verification loop-invariant formal-semantics hoare-logic 2014-10-11

    4熱度

    1回答

    Python中的程序驗證

    我正在教授關於FOL和程序驗證的課程，這本書的靈感來自Mordechai Ben-Ari，計算機科學的數學邏輯，Springer，1993-2012。我想通過讓學生用Python編程來說明概念。 對於FOL我使用NLTK，它有一個很好的FOL包。 但我還沒有找到一個Python包程序驗證：將先決條件和後置條件邏輯公式，發現循環不變，驗證由步驟，等等。換句話說Python程序步驟，使用霍爾邏輯Pyt
    python hoare-logic 2014-02-10

    1熱度

    1回答

    Hoare邏輯，while循環與'<='

    我正在研究一些Hoare邏輯，我想知道我的方法是否正確。 我有以下程序P： s = 0 i = 1 while (i <= n) { s = s + i i = i + 1 } 應該滿足霍爾三重{N> = 0} p {S = N *（N + 1）/ 2}（因此它只是需要的和）。現在，最初我有| s = i *（i-1）/ 2 |作爲我的不變，這工作正常。但是，我的循環
    while-loop invariants hoare-logic 2012-01-27

    2熱度

    1回答

    Z3中if-else和while循環的驗證條件

    我正在學習Z3並希望輸入Hoare邏輯所述的一些驗證條件，並獲得給定Hoare三元組的模型。 到目前爲止，我只能夠驗證任務，這裏有一個例子（只是爲了檢查，如果我這樣做是正確的）： Given: { x< 40 } x :=x+10 { x < 50} (declare-const x Int) (assert (< x 50)) (assert (< (+ x 10) 50)) (check
    z3 hoare-logic 2015-05-07
最新問題