2,619
次編輯
「Dafny雜記」修訂間的差異
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 39： | 行 39： | ||
Hello，汝好 | Hello，汝好 | ||
</pre> | </pre> | ||
==Án-tsuánn 用 Dafny 做驗證？== | |||
通常驗證tsit 段程式，ē當用 Hoare 邏輯來驗證（通參考[https://flolac.iis.sinica.edu.tw/flolac12/lib/exe/flolac12.pdf 中央研究院ê FLOLAC投影片]）。若是驗證一段（tsi̍t tsuā以上）ê程式P，著知影precondition（執行進前ê條件）、postsondition（執行了後ê情況，寫做： | |||
{PreCondition}{P}{PostCondition} | |||
例： | |||
<pre> | |||
{x == old(x)}{x := x + 1}{x > old(x)} | |||
x == old(x) 是 P ê Precondition，PostCondition sī x > old(x)。 | |||
</pre> | |||
Tsit pîng無講siūnn tsē，只是tsit ê輔助：dafny 驗證ê時陣，著先指定下kha三項假設，koh請程式驗證正確無： | |||
# Precondition | |||
# Costcondition | |||
# Loop Invariant（循環無變式）：佇loop內底逐kái執行，無變ê表達式。虛擬碼ê例：<code>for (var i=0 to 4){print(i);};</code>，<code>i<=4 & i>=0</code>就是 loop invatriant。 | |||
== 參考 == | == 參考 == | ||