「Dafny雜記」修訂間的差異

Dafny雜記 (檢視原始碼)

增加 27 位元組、 2023年8月10日 (四) 02:55

2,617

次編輯

@@ 行 56： / 行 56： @@
 # 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。
+# Loop Invariant（循環無變式）：逐kái執行loop，tī tsit ê loop ê「逐位」lóng無變ê表達式。虛擬碼ê例：<code>for (var i=0 to 4){print(i);};</code>，<code>i<=4 & i>=0</code>就是 loop invatriant。
 == 參考 ==