daily pastebin goal
31%
SHARE
TWEET

Untitled

a guest Jan 19th, 2019 50 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. function sum( n :Z) : Z
  2.     precondition n_ge_one : n >=1
  3.     postcondition sum=n*(n+1)/2
  4.     var x : Z
  5.         y : Z
  6. begin
  7.     { x = x /\ n >= 1 }
  8.     x := 1
  9.     { x = 1 /\ n >= 1 }
  10.     { y = y /\ x = 1 /\ n>=1 }
  11.     y := 0
  12.     { y = 0 /\ x = 1 /\ n>=1 }
  13.     while x <= n do
  14.     invariant y = (x-1)*x/2 /\ n>=1 /\ x <= n + 1
  15.     begin
  16.         { y + x = (x-1)*x/2 + x /\ n>=1 /\ x < n + 1 }
  17.         y := y + x
  18.         { y = (x-1)*x/2 + x /\ n>=1 }
  19.         { y = (x + 1 - 2)*(x + 1 - 1)/2 + x + 1 - 1 /\ n>=1 /\ x < n + 1}
  20.         x := x + 1
  21.         { y = (x-2)*(x-1)/2 + x-1 /\ n>=1 /\ x <= n + 1}
  22.     end
  23.     { y = n*(n+1)/2}
  24.     sum := y
  25.     { sum = n*(n+1)/2}
  26. end
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top