header {* 
  \isaheader{Safety Policy against arithmetic overflow} 
*}

theory JBC_SafetyPolicy = JBC_Semantics:


constdefs
MAX :: int
"MAX \<equiv> 2147483647"

MX :: val
"MX \<equiv> Intg MAX"

constdefs safeF::"jbc_prog \<Rightarrow> pos \<Rightarrow> expr"
"safeF \<Pi> p \<equiv> (case (cmd \<Pi> p) of None \<Rightarrow> FF
| Some c \<Rightarrow> case c 
of Load nat \<Rightarrow> TT 
| Store nat \<Rightarrow> TT 
| Push val \<Rightarrow> TT
| New cname \<Rightarrow> TT
| Getfield vname cname \<Rightarrow> TT
| Putfield vname cname \<Rightarrow> TT
| Checkcast cname \<Rightarrow> TT
| Invoke mname nat \<Rightarrow> TT
| Return \<Rightarrow> TT
| Pop \<Rightarrow> TT
| (IBin no) \<Rightarrow> Rel (Num (St 1) no (St 0)) Leq (Cn MX)
| Goto int \<Rightarrow> TT
| CmpEq \<Rightarrow> TT
| IfIntCmp ro b \<Rightarrow> TT
| IfFalse int \<Rightarrow> TT
| Throw \<Rightarrow> TT)"

constdefs sys_xcptns :: "cname list"
"sys_xcptns  \<equiv>  [NullPointer, ClassCast, OutOfMemory]"

constdefs initF::"jbc_prog \<Rightarrow> expr"
"initF \<Pi> == And ([Pos (ipc \<Pi>),Eq (Rg 0) (Cn Null),Eq FrNr (Cn (Intg 1))]@
 (map (\<lambda>C. Ty (Cn (Addr (addr_of_sys_xcpt C))) (Class C)) sys_xcptns)@
 (let (C,M,pc)=ipc \<Pi>;
     (D,Ts,T,mxs,mxl,bd) = method (fst \<Pi>) C M
 in map (\<lambda>n. not_none (Rg n)) (upt 1 (Suc mxl))))"
(* "initF \<Pi> \<equiv> And ([Pos (ipc \<Pi>),Eq (Rg 0) (Cn Null),Eq FrNr (Cn (Intg 1))]@
 (map (\<lambda>C. Ty (Cn (Addr (addr_of_sys_xcpt C))) (Class C)) sys_xcptns))" *)

end