src/HOL/IMP/Abs_Int_Tests.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58410 6d46ad54a2ab
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 theory Abs_Int_Tests
     2 imports Com
     3 begin
     4 
     5 subsection "Test Programs"
     6 
     7 text{* For constant propagation: *}
     8 
     9 text{* Straight line code: *}
    10 definition "test1_const =
    11  ''y'' ::= N 7;;
    12  ''z'' ::= Plus (V ''y'') (N 2);;
    13  ''y'' ::= Plus (V ''x'') (N 0)"
    14 
    15 text{* Conditional: *}
    16 definition "test2_const =
    17  IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
    18 
    19 text{* Conditional, test is relevant: *}
    20 definition "test3_const =
    21  ''x'' ::= N 42;;
    22  IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
    23 
    24 text{* While: *}
    25 definition "test4_const =
    26  ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
    27 
    28 text{* While, test is relevant: *}
    29 definition "test5_const =
    30  ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
    31 
    32 text{* Iteration is needed: *}
    33 definition "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 
    37 text{* For intervals: *}
    38 
    39 definition "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 
    45 definition "test2_ivl =
    46  WHILE Less (V ''x'') (N 100)
    47  DO ''x'' ::= Plus (V ''x'') (N 1)"
    48 
    49 definition "test3_ivl =
    50  ''x'' ::= N 0;;
    51  WHILE Less (V ''x'') (N 100)
    52  DO ''x'' ::= Plus (V ''x'') (N 1)"
    53 
    54 definition "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 
    59 definition "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 
    64 definition "test6_ivl =
    65  ''x'' ::= N 0;;
    66  WHILE Less (N (- 1)) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
    67 
    68 end