「Dafny雜記」修訂間的差異

Dafny雜記 (檢視原始碼)

增加 722 位元組、 2023年8月10日 (四) 03:15

無編輯摘要

2,617

次編輯

@@ 行 57： / 行 57： @@
 # Costcondition
 # 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。
+例：
+<pre>
+/* add1ToN(n) = 1 + 2 + ... + n, n>0 */
+method add1ToN(n : nat) returns (res: nat) //n : input value; res : return value
+    requires n > 0 // define the precondition
+    ensures res > res - 10// define the  postcondition
+{
+    res := 0;
+    var i : nat := 1; // the item of while
+    // loop
+    while (i < n)
+    // set the invariant of the loop
+    /* bacause when i = n-1 into the loop, it'll become n after Flag A.
+    so the invariant is "1 <= i <= n" */
+        invariant 1 <= i <= n
+        // the loop expression n-i is decreasing
+        decreases n-i
+        {
+            res := res + i;
+            i := i + 1; // Flag A
+        }
+    res := res + n;
+    return res; // return x
+}</pre>
 == 參考 ==