API tools faq
paste
Advertisement
Guest User

Proof

a guest
Dec 18th, 2018
73
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 2.13 KB | None | 0 0
raw download clone embed print report
  1. First prove the invariant holds when entering the loop:
  2. Q ==> wp(res:=1;i:=2, I)
  3.  
  4. n > 0 ==> wp(res:=1;i:=2, res == fact(i - 1) && (i <= n + 1))
  5. //sequential followed by assignments
  6. n > 0 ==> 1 == fact(2 - 1) && (2 <= n + 1)
  7. n > 0 ==> 1 == 1 && (n => 1)
  8. n > 0 ==> n > 0
  9. true
  10.  
  11. Second prove that the invarinat is preserved by the loop:
  12. I && B ==> wp(res := res * i; i := i + 1, I)
  13.  
  14. ((res == fact(i - 1) && (i <= n + 1)) && (i <= n)) ==> wp(res := res * i; i := i + 1, (res == fact(i - 1) && (i <= n + 1))
  15. //sequential followed by assignments
  16. ((res == fact(i - 1) && (i <= n + 1)) && (i <= n)) ==> (res * i == fact(i + 1 - 1) && (i + 1 <= n + 1))
  17. ((res == fact(i - 1) && (i <= n)) ==> (res * i == fact(i) && (i <= n))
  18. ((res == fact(i - 1) && (i <= n)) ==> (res == fact(i)/i && (i <= n))
  19. ((res == fact(i - 1) && (i <= n)) ==> (res == fact(i - 1) && (i <= n))
  20. true
  21.  
  22. Third prove that the postcondition hold after loop exits:
  23. I && !B ==> R
  24.  
  25. (res == fact(i - 1) && (i <= n + 1)) && (i > n) ==> (res == fact(n))
  26. (res == fact(i - 1)) && (i <= n + 1) && (i => n + 1) ==> (res == fact(n))
  27. (res == fact(i - 1)) && (i == n + 1) ==> (res == fact(n))
  28. (res == fact(n + 1 - 1)) ==> (res == fact(n))
  29. (res == fact(n)) ==> (res == fact(n))
  30. true
  31.  
  32. Fourth prove that the variant is bounded form below by 0, as long as the loop has not terminated:
  33. I && B ==> D > 0
  34.  
  35. (res == fact(i - 1) && (i <= n + 1)) && (i <= n) ==> ((n - i) + 1) > 0
  36. (res == fact(i - 1) && (i <= n) ==> (n - i >= 0)
  37. (res == fact(i - 1) && (0 <= n - i) ==> (n - i >= 0)
  38. //implication rule
  39. !((res == fact(i - 1) && (0 <= n - i)) || (n - i >= 0)
  40. //de Morgan rule
  41. !(res == fact(i - 1)) || !(0 <= n - i) || (n - i >= 0)
  42. //inverse rule
  43. !(res == fact(i - 1)) || true
  44. //annihilation
  45. true
  46.  
  47. Fifth prove that the variant decrease on each loop iteration.
  48. I && B ==> wp(tmp := D; S, tmp > D)
  49.  
  50. (res == fact(i - 1) && (i <= n + 1)) && (i <= n) ==> wp(tmp := n - i + 1; res:= res * i; i := i + 1, tmp > n - i + 1)
  51. //sequentials followed by assignments
  52. (res == fact(i - 1) && (i <= n + 1)) && (i <= n) ==> n - i + 1 > n - i + 2
  53. (res == fact(i - 1) && (i <= n + 1)) && (i <= n) ==> true
  54. trivially true
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
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
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!