equal
deleted
inserted
replaced
44 *} |
44 *} |
45 constdefs |
45 constdefs |
46 start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" |
46 start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" |
47 "start_state G C m \<equiv> |
47 "start_state G C m \<equiv> |
48 let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in |
48 let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in |
49 (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])" |
49 (None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])" |
50 |
50 |
51 end |
51 end |