Guest User

Benjam

a guest
Jan 15th, 2020
66
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. CONSTANTS
  2. x0,
  3. deltaX,
  4. y0,
  5. deltaY
  6. PROPERTIES
  7. x0:NAT &
  8. x0<=MAXINT &
  9. x0>=0&
  10. deltaX:NAT &
  11. x0+deltaX<=MAXINT &
  12. y0:NAT &
  13. y0<=MAXINT &
  14. y0>=0 &
  15. deltaY:NAT &
  16. y0+deltaY<=MAXINT
  17. VARIABLES
  18. xx,
  19. yy
  20. INVARIANT
  21. xx:NAT & deltaX+x0>=xx
  22. & yy:NAT & deltaY+y0>=yy
  23. INITIALISATION
  24. xx:=0
  25. || yy:=0
  26.  
  27. OPERATIONS
  28. setX(nx)=
  29. PRE nx:NAT & nx<= MAXINT & nx<=deltaX+x0
  30. THEN xx:=nx
  31. END;
  32.  
  33. incX(val)=
  34. PRE val:NAT & val<=MAXINT & xx+val<=MAXINT & val+xx<=deltaX+x0
  35. THEN xx:= val+xx
  36. END;
  37.  
  38. decrX(val)=
  39. PRE val:NAT & val<=MAXINT & xx-val>=x0
  40. THEN xx:= xx-val
  41. END;
  42.  
  43. setY(ny)=
  44. PRE ny:NAT & ny<= MAXINT & ny<=deltaY+y0
  45. THEN yy:=ny
  46. END;
  47.  
  48. incY(val)=
  49. PRE val:NAT & val<=MAXINT & yy+val<=MAXINT & val+yy<=deltaY+y0
  50. THEN yy:= val+yy
  51. END;
  52.  
  53. decrY(val)=
  54. PRE val:NAT & val<=MAXINT & yy-val>=y0
  55. THEN yy:= yy-val
  56. END;
  57.  
  58. val<--getX=
  59. BEGIN
  60. val:=xx
  61. END;
  62.  
  63. val<--getY=
  64. BEGIN
  65. val:=yy
  66. END;
  67.  
  68. val<--borneX(ux)=
  69. PRE ux:NAT
  70. THEN
  71. val:=bool(ux>=x0 & ux<=x0+deltaX)
  72. END;
  73.  
  74. val<--borneY(uy)=
  75. PRE uy:NAT
  76. THEN
  77. val:=bool(uy>=x0 & uy<=x0+deltaY)
  78. END
RAW Paste Data