theory EX_Sum =  VCGExec:

section {* Example - Sum *}

subsection {* Name Declarations *}

constdefs
 Adder :: cname
 "Adder \<equiv> ''Adder''"
 sum :: mname
 "sum \<equiv> ''sum''"
 n::"vname"
 "n \<equiv> ''n''"
 this::nat
 "this \<equiv> 0"
 k::nat
 "k\<equiv>1"
 res::nat
 "res\<equiv>2"

--{* \clearpage *}

subsection {* Program Code *}

consts comment ::"instr \<Rightarrow> string \<Rightarrow> instr" ("(_ -- _)" [61,60] 60)
defs comment_def [simp]:
"comment i s \<equiv> i"

constdefs arg::"int"
"arg \<equiv> 65535"

constdefs
 StartC :: "jvm_method cdecl"
 "StartC \<equiv> (Start,(Object, [],[(main,[],Integer,(2,2,[
 New Adder,
 Store 1,
 Load 1,
 Push (Intg arg),
 Putfield n Adder,
 Load 1,
 Invoke sum 0 -- ''main_call'',
 Return -- ''main_ret'', 
 Push (Intg -1), Return -- ''handler for NullPointer Ex.'' ,
 Push (Intg -1), Return -- ''handler for ClassCast Ex.'',
 Push (Intg -1), Return -- ''handler for OutOfMemory Ex.''],
 [(0,7,NullPointer,8,0),
  (0,7,ClassCast,10,0),
  (0,7,OutOfMemory,12,0)]))]))"

constdefs
  AdderC :: "jvm_method cdecl"
  "AdderC \<equiv> (Adder, (Object,[(n,Integer)],[
(sum,[],Integer,(2,2,[
  Push (Intg 0) -- ''sum_pre'' , 
  Store k,
  Push (Intg 0),
  Store res,
  Load k -- ''sum_inv'',
  Load this,
  Getfield n Adder,
  IfIntLeq 10,
  Load k,
  Push (Intg 1),
  IAdd,
  Store k,
  Load res,
  Load k,
  IAdd,
  Store res,
  Goto -12 -- ''jumps to sum_inv'', 
  Load res,
  Return -- ''sum_post''],[]))]))"

--{* \clearpage *}

subsection {* Annotations *}

constdefs
 main_call::"expr"
 "main_call \<equiv> And [Gf n Adder (St 0) \<doteq> Cn (Intg arg)]"
 main_ret::"expr"
 "main_ret \<equiv> St 0 \<doteq> Cn (Intg ((arg * (arg+1)) div 2))"
 sum_pre::"expr"
 "sum_pre \<equiv> And [ Ty (Gf n Adder (Rg 0)) Integer, Rg 0 \<doteq> Call (St 0), 
  Gf n Adder (Rg 0) \<doteq> Call (Gf n Adder (St 0)), 
  (Gf n Adder (Rg 0)) \<preceq> (Cn (Intg 65535)), 
  (Cn (Intg 0)) \<preceq> (Gf n Adder (Rg 0)) ]"
 sum_inv::"expr"
 "sum_inv \<equiv> And [ Ty (Gf n Adder (Rg 0)) Integer, 
  ((Cn (Intg 2)) \<otimes> (Rg res)) \<doteq> (Rg k \<otimes> (Rg k \<oplus> (Cn (Intg 1)))), 
  Gf n Adder (Rg 0) \<doteq> Call (Gf n Adder (St 0)), 
  (Gf n Adder (Rg 0)) \<preceq> (Cn (Intg 65535)), 
  (Cn (Intg 0)) \<preceq> (Gf n Adder (Rg 0)), Rg k \<preceq> (Gf n Adder (Rg 0)), 
  (Cn (Intg 0)) \<preceq> Rg k]"

 sum_post::"expr"
 "sum_post \<equiv> And [Ty (Gf n Adder (Rg 0)) Integer, St 0 \<doteq> Rg res, 
  Gf n Adder (Rg 0) \<doteq> Call (Gf n Adder (St 0)),  
  ((Cn (Intg 2)) \<otimes> (Rg res)) \<doteq>  
  ((Call (Gf n Adder (St 0))) \<otimes> ((Call (Gf n Adder (St 0))) \<oplus> (Cn (Intg 1))))]"


subsection {* Packing code and annotations *}

constdefs
prog::"jbc_prog"
"prog \<equiv> (SystemClasses @ [AdderC,StartC],
 [((Start,main,6),main_call),
  ((Start,main,7),main_ret),
  ((Start,main,8),TT),
  ((Start,main,10),TT),
  ((Start,main,12),TT),
  ((Adder,sum,0),sum_pre),
  ((Adder,sum,4),sum_inv),
  ((Adder,sum,18),sum_post)])"

--{* \clearpage *}


subsection {* Generate ML code for the VCG *}

generate_code ("EX_Sum.ML") [term_of]
  wf_jvm_prog_phi = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phi \<Phi> P"
  wf = "wf"
  opt = "opt"
  vcg = "vcgTy"
  prog = "prog"

 
--{* If a program is not wellformed, the following
     functions help to find out why. *}
  
  phi_prog = "map_of2 (convert_pt (prog_kil (fst prog)))"
  wfS = "wfS"
  wf_jvm_prog_phiS = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phiS \<Phi> P"
  initjob = "initjob (fst prog) Start ''main''"
  nxtjob = "nxtjob  (fst prog) Start ''main''"
  printjob = "\<lambda> job. printjob (fst prog) Start ''main'' job"
  parsejob = "parsejob"

subsection {* Verification Condition *}

ML {* use "EX_Sum.ML" *}
ML {* wf prog; *}
ML {* val vc = opt (vcg prog); *}
ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_expr vc))); *}

--{* now we trasfer the ML result back to Isabelle *}
ML_setup {*
val t = term_of_expr vc;
val T = fastype_of t;
Context.>> (fn thy => thy |>
  Theory.add_consts_i [("vc", T, NoSyn)] |>
  (fst o PureThy.add_defs_i false [(("vc_def", Logic.mk_equals (Const ("EX_Sum.vc", T), t)), [])]));
*}

--{* the verification condition is now defined as constant vc::expr *}

section {* Proving the Verification Condition *}

text {* Here we prove the vc (via the semantics of formulae). The evaluation simpset from VCGexec.thy is tuned for this
        purpose. Some of the evaluation rules (evalEevalEs.simps) are ommitted, because
        this keeps the expansion overhead small.\\[1ex] *}

text {* The following lemma is used for the verification of the example. Alternatively
        one could use a tactic for bounded arithemtics. *}

lemma special_bounded_mult: "\<lbrakk> 2 * (a::int) = b * (b+1); 0 \<le> (b::int); b \<le> c \<rbrakk> \<Longrightarrow>  b + a \<le> c + ((c * (c + 1)) div 2)"
(*<*)
apply (rule_tac c="2" in mult_left_le_imp_le)
 prefer 2
 apply simp
apply (simp add: zadd_zmult_distrib2)
apply (subgoal_tac "even (c * c + c)")
 prefer 2
 apply simp
apply (simp add: two_times_even_div_two)
apply (subgoal_tac "((3 * b) + (b * b)) \<le> ((3 * c) + (c * c))")
 prefer 2
 apply (rule add_mono)
 apply simp
 apply (rule mult_mono)
 apply simp
 apply simp
 apply simp
 apply simp
apply simp
done 
(*>*)

declare evalE_evalEs.simps [simp del]
declare sem_simps [simp add]

lemma vcg_prog_holds:
"prog \<turnstile> vc"
apply (simp only: provable_def vc_def)
apply (safe intro!: And0 AndI')
txt {* @{subgoals [display, indent=0, margin=90]} *}
apply (simp only: deriv_def, rule ballI, clarsimp |
       drule_tac c="65534" in  special_bounded_mult | 
       simp add:  zadd_zmult_distrib zadd_zmult_distrib2 )+
--{* nprfsize = 101768 *}
done

end