1theory Abs_Int_Tests
2imports Com
3begin
4
5subsection "Test Programs"
6
7text\<open>For constant propagation:\<close>
8
9text\<open>Straight line code:\<close>
10definition "test1_const =
11 ''y'' ::= N 7;;
12 ''z'' ::= Plus (V ''y'') (N 2);;
13 ''y'' ::= Plus (V ''x'') (N 0)"
14
15text\<open>Conditional:\<close>
16definition "test2_const =
17 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
18
19text\<open>Conditional, test is relevant:\<close>
20definition "test3_const =
21 ''x'' ::= N 42;;
22 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
23
24text\<open>While:\<close>
25definition "test4_const =
26 ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
27
28text\<open>While, test is relevant:\<close>
29definition "test5_const =
30 ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
31
32text\<open>Iteration is needed:\<close>
33definition "test6_const =
34  ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;;
35  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')"
36
37text\<open>For intervals:\<close>
38
39definition "test1_ivl =
40 ''y'' ::= N 7;;
41 IF Less (V ''x'') (V ''y'')
42 THEN ''y'' ::= Plus (V ''y'') (V ''x'')
43 ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
44
45definition "test2_ivl =
46 WHILE Less (V ''x'') (N 100)
47 DO ''x'' ::= Plus (V ''x'') (N 1)"
48
49definition "test3_ivl =
50 ''x'' ::= N 0;;
51 WHILE Less (V ''x'') (N 100)
52 DO ''x'' ::= Plus (V ''x'') (N 1)"
53
54definition "test4_ivl =
55 ''x'' ::= N 0;; ''y'' ::= N 0;;
56 WHILE Less (V ''x'') (N 11)
57 DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N 1))"
58
59definition "test5_ivl =
60 ''x'' ::= N 0;; ''y'' ::= N 0;;
61 WHILE Less (V ''x'') (N 100)
62 DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
63
64definition "test6_ivl =
65 ''x'' ::= N 0;;
66 WHILE Less (N (- 1)) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
67
68end
69