2,617
次編輯
「Dafny雜記」修訂間的差異
跳至導覽
跳至搜尋
→Án-tsuánn 用 Dafny 做驗證？
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 47： | 行 47： | ||
例： | 例： | ||
{x == old(x)}{x := x + 1}{x > old(x)} | <pre>{x == old(x)}{x := x + 1}{x > old(x)}</pre> | ||
其中，x == old(x) 是 P ê Precondition，PostCondition sī x > old(x)。 | |||
Tsit pîng無講siūnn tsē，只是tsit ê輔助：dafny 驗證ê時陣，著先指定下kha三項假設，koh請程式驗證正確無： | Tsit pîng無講siūnn tsē，只是tsit ê輔助：dafny 驗證ê時陣，著先指定下kha三項假設，koh請程式驗證正確無： | ||
| 行 58： | 行 57： | ||
# Costcondition | # Costcondition | ||
# Loop Invariant（循環無變式）：佇loop內底逐kái執行，無變ê表達式。虛擬碼ê例：<code>for (var i=0 to 4){print(i);};</code>，<code>i<=4 & i>=0</code>就是 loop invatriant。 | # Loop Invariant（循環無變式）：佇loop內底逐kái執行，無變ê表達式。虛擬碼ê例：<code>for (var i=0 to 4){print(i);};</code>，<code>i<=4 & i>=0</code>就是 loop invatriant。 | ||
== 參考 == | == 參考 == | ||