theory EX_MainSumAuto = VCGExec:

section {* Definitions *}

subsection {* Name Declarations *}

constdefs
 this::nat
 "this \<equiv> 0"
 k::nat
 "k\<equiv>2"
 n::nat
 "n \<equiv> 1"
 res::nat
 "res\<equiv>3"

subsection {* Program Code *}

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

constdefs sum::cname
"sum \<equiv> ''sum''"

constdefs
 StartCR :: "jvm_method cdecl"
 "StartCR \<equiv> (Start,(Object, [],[(main,[],Integer,(1,1,[Push (Intg 5),Return],[])),
(sum,[Integer],Integer,(2,4,[
 Push (Intg 0),
 Store res,
 Push (Intg 0),
 Store k,
 Load n,
 Push (Intg 65536),
 IfIntLeq 16,
 Load k --''LOOP : sum_inv '',
 Load n,
 IfIntLeq 13 -- ''if n <= k then goto EXIT else k++; res+=k; goto LOOP'' ,
 Load res,
 Push (Intg 2147418113) --  ''maximum value Rg res can have at this position without causing an overflow'',
 IfIntLeq 10,
 Load k ,
 Push (Intg 1),
 IAdd,
 Store k,
 Load k,
 Load res,
 IAdd,
 Store res,
 Goto (-14) -- ''goto LOOP'',
 Load res -- ''EXIT'',
 Return ],
 []))]))"

constdefs
prog::"jbc_prog"
"prog \<equiv> (SystemClasses @ [StartCR],[])"

subsection {* Generating ML Code *}

(* Turn off longnames! *)

generate_code ("EX_MainSumAuto.ML") [term_of]
  exprg = "exprg"
  phi_exprg = "map_of2 (convert_pt (prog_kil exprg))"
  wf_jvm_prog_phi = "\<lambda> \<Phi> (P::jvm_prog). wf_jvm_prog_phi \<Phi> P"
  wf = "wf"
  opt = "opt"
  vcg = "vcgTy"
  prog = "prog"
  phi_prog = "map_of2 (convert_pt (prog_kil (fst prog)))"
  initjob = "initjob (fst prog) Start ''sum''"
  nxtjob = "nxtjob  (fst prog) Start ''sum''"
  printjob = "\<lambda> job. printjob (fst prog) Start ''sum'' job"
  parsejob = "parsejob"

subsection {* Generate  annotations *}

ML {* print_depth 100 *}
ML {* use "pa_sources" *}
ML {* use_src "/home/wiss/wildmosm/work/PA/JVM/" "EX_MainSumAuto"; *}
ML {* val aprog = interval_analyzeprog prog; *}
ML {* aprog; *}


subsection {* Computing and verifying the verification condition *}

ML {* wf aprog; *}
ML {* val vc = opt (vcg aprog); *}

--{* 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_MainSumAuto.vc", T), t)), [])]));
*}

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

lemma vc_prg_holds:
"prog \<turnstile> vc"
apply (simp only: provable_def vc_def)
apply (safe intro!: And0 AndI')
apply (simp only: deriv_def, rule ballI, clarsimp simp del: evalE_evalEs.simps simp add: sem_simps)
done

end