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