src/HOL/IMP/Abs_Int_Tests.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46432 ce8f7944fd6b
child 49095 7df19036392e
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     1
theory Abs_Int_Tests
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     2
imports ACom
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     3
begin
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     4
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     5
subsection "Test Programs"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     6
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     7
text{* For constant propagation: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     8
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     9
text{* Straight line code: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    10
definition "test1_const =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    11
 ''y'' ::= N 7;
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    12
 ''z'' ::= Plus (V ''y'') (N 2);
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    13
 ''y'' ::= Plus (V ''x'') (N 0)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    14
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    15
text{* Conditional: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    16
definition "test2_const =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    17
 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    18
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    19
text{* Conditional, test is relevant: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    20
definition "test3_const =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    21
 ''x'' ::= N 42;
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    22
 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    23
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    24
text{* While: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    25
definition "test4_const =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    26
 ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    27
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    28
text{* While, test is relevant: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    29
definition "test5_const =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    30
 ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    31
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    32
text{* Iteration is needed: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    33
definition "test6_const =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    34
  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    35
  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    36
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    37
text{* For intervals: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    38
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    39
definition "test1_ivl =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    40
 ''y'' ::= N 7;
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    41
 IF Less (V ''x'') (V ''y'')
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    42
 THEN ''y'' ::= Plus (V ''y'') (V ''x'')
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    43
 ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    44
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    45
definition "test2_ivl =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    46
 WHILE Less (V ''x'') (N 100)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    47
 DO ''x'' ::= Plus (V ''x'') (N 1)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    48
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    49
definition "test3_ivl =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    50
 ''x'' ::= N 7;
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    51
 WHILE Less (V ''x'') (N 100)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    52
 DO ''x'' ::= Plus (V ''x'') (N 1)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    53
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    54
definition "test4_ivl =
46432
nipkow
parents: 45623
diff changeset
    55
 ''x'' ::= N 0; ''y'' ::= N 0;
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    56
 WHILE Less (V ''x'') (N 11)
46432
nipkow
parents: 45623
diff changeset
    57
 DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N 1))"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    58
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    59
definition "test5_ivl =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    60
 ''x'' ::= N 0; ''y'' ::= N 0;
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    61
 WHILE Less (V ''x'') (N 1000)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    62
 DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    63
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    64
definition "test6_ivl =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    65
 ''x'' ::= N 0;
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    66
 WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    67
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    68
end