src/HOL/IMP/Abs_Int0_const.thy
author nipkow
Wed Sep 28 09:55:11 2011 +0200 (2011-09-28)
changeset 45111 054a9ac0d7ef
child 45127 d2eb07a1e01b
permissions -rw-r--r--
Added Hoare-like Abstract Interpretation
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Abs_Int0_const
     4 imports Abs_Int0
     5 begin
     6 
     7 subsection "Constant Propagation"
     8 
     9 datatype cval = Const val | Any
    10 
    11 fun rep_cval where
    12 "rep_cval (Const n) = {n}" |
    13 "rep_cval (Any) = UNIV"
    14 
    15 fun plus_cval where
    16 "plus_cval (Const m) (Const n) = Const(m+n)" |
    17 "plus_cval _ _ = Any"
    18 
    19 lemma plus_cval_cases: "plus_cval a1 a2 =
    20   (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
    21 by(auto split: prod.split cval.split)
    22 
    23 instantiation cval :: SL_top
    24 begin
    25 
    26 fun le_cval where
    27 "_ \<sqsubseteq> Any = True" |
    28 "Const n \<sqsubseteq> Const m = (n=m)" |
    29 "Any \<sqsubseteq> Const _ = False"
    30 
    31 fun join_cval where
    32 "Const m \<squnion> Const n = (if n=m then Const m else Any)" |
    33 "_ \<squnion> _ = Any"
    34 
    35 definition "\<top> = Any"
    36 
    37 instance
    38 proof
    39   case goal1 thus ?case by (cases x) simp_all
    40 next
    41   case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
    42 next
    43   case goal3 thus ?case by(cases x, cases y, simp_all)
    44 next
    45   case goal4 thus ?case by(cases y, cases x, simp_all)
    46 next
    47   case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
    48 next
    49   case goal6 thus ?case by(simp add: Top_cval_def)
    50 qed
    51 
    52 end
    53 
    54 interpretation Rep rep_cval
    55 proof
    56   case goal1 thus ?case
    57     by(cases a, cases b, simp, simp, cases b, simp, simp)
    58 next
    59   case goal2 show ?case by(simp add: Top_cval_def)
    60 qed
    61 
    62 interpretation Val_abs rep_cval Const plus_cval
    63 proof
    64   case goal1 show ?case by simp
    65 next
    66   case goal2 thus ?case
    67     by(auto simp: plus_cval_cases split: cval.split)
    68 next
    69   case goal3 thus ?case
    70     by(auto simp: plus_cval_cases split: cval.split)
    71 qed
    72 
    73 text{* Could set the limit of the number of iterations to an arbitrarily
    74 large number because all ascending chains in this semilattice are finite. *}
    75 
    76 interpretation Abs_Int rep_cval Const plus_cval "(iter 15)"
    77 defines AI_const is AI
    78 and aval'_const is aval'
    79 and step_const is step
    80 proof qed (auto simp: iter_pfp strip_iter)
    81 
    82 text{* Straight line code: *}
    83 definition "test1_const =
    84  ''y'' ::= N 7;
    85  ''z'' ::= Plus (V ''y'') (N 2);
    86  ''y'' ::= Plus (V ''x'') (N 0)"
    87 
    88 text{* Conditional: *}
    89 definition "test2_const =
    90  IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
    91 
    92 text{* Conditional, test is ignored: *}
    93 definition "test3_const =
    94  ''x'' ::= N 42;
    95  IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
    96 
    97 text{* While: *}
    98 definition "test4_const =
    99  ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
   100 
   101 text{* While, test is ignored: *}
   102 definition "test5_const =
   103  ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
   104 
   105 text{* Iteration is needed: *}
   106 definition "test6_const =
   107   ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
   108   WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
   109 
   110 text{* More iteration would be needed: *}
   111 definition "test7_const =
   112   ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
   113   WHILE Less (V ''x'') (N 1)
   114   DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
   115 
   116 text{* For readability: *}
   117 translations "x" <= "CONST V x"
   118 translations "x" <= "CONST N x"
   119 translations "x" <= "CONST Const x"
   120 translations "x < y" <= "CONST Less x y"
   121 translations "x" <= "CONST B x"
   122 translations "x" <= "CONST Up x"
   123 
   124 value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
   125 value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
   126 value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
   127 value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
   128 value [code] "show_acom (AI_const test1_const)"
   129 
   130 value [code] "show_acom (AI_const test2_const)"
   131 value [code] "show_acom (AI_const test3_const)"
   132 
   133 value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
   134 value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
   135 value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
   136 value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
   137 value [code] "show_acom (AI_const test4_const)"
   138 
   139 value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
   140 value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
   141 value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))"
   142 value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
   143 value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
   144 value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
   145 value [code] "show_acom (AI_const test5_const)"
   146 
   147 value [code] "show_acom (AI_const test6_const)"
   148 value [code] "show_acom (AI_const test7_const)"
   149 
   150 end