Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- function sum( n :Z) : Z
- precondition n_ge_one : n >=1
- postcondition sum=n*(n+1)/2
- var x : Z
- y : Z
- begin
- { x = x /\ n >= 1 }
- x := 1
- { x = 1 /\ n >= 1 }
- { y = y /\ x = 1 /\ n>=1 }
- y := 0
- { y = 0 /\ x = 1 /\ n>=1 }
- while x <= n do
- invariant y = (x-1)*x/2 /\ n>=1 /\ x <= n + 1
- begin
- { y + x = (x-1)*x/2 + x /\ n>=1 /\ x < n + 1 }
- y := y + x
- { y = (x-1)*x/2 + x /\ n>=1 }
- { y = (x + 1 - 2)*(x + 1 - 1)/2 + x + 1 - 1 /\ n>=1 /\ x < n + 1}
- x := x + 1
- { y = (x-2)*(x-1)/2 + x-1 /\ n>=1 /\ x <= n + 1}
- end
- { y = n*(n+1)/2}
- sum := y
- { sum = n*(n+1)/2}
- end
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement