• API
• FAQ
• Tools
• Archive
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.
Not a member of Pastebin yet?