SHARE
TWEET

Benjam

a guest Jan 15th, 2020 62 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
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!
 
Top