src/HOL/MicroJava/JVM/JVMState.thy
changeset 10057 8c8d2d0d3ef8
parent 10042 7164dc0d24d8
child 10922 f1209aff9517
     1.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Thu Sep 21 19:25:57 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Fri Sep 22 13:12:19 2000 +0200
     1.3 @@ -2,25 +2,26 @@
     1.4      ID:         $Id$
     1.5      Author:     Cornelia Pusch
     1.6      Copyright   1999 Technische Universitaet Muenchen
     1.7 -
     1.8 -State of the JVM
     1.9  *)
    1.10  
    1.11 -JVMState = Store +
    1.12 +
    1.13 +header {* State of the JVM *}
    1.14  
    1.15  
    1.16 -(** frame stack **)
    1.17 +theory JVMState = Store:
    1.18  
    1.19 +
    1.20 +text {* frame stack :*}
    1.21  types
    1.22   opstack 	 = "val list"
    1.23   locvars 	 = "val list" 
    1.24   p_count 	 = nat
    1.25  
    1.26 - frame = "opstack \\<times>			
    1.27 -	  locvars \\<times>		
    1.28 -	  cname \\<times>			
    1.29 -	  sig \\<times>			
    1.30 -	  p_count"
    1.31 + frame = "opstack \<times>			
    1.32 +          locvars \<times>		
    1.33 +          cname \<times>			
    1.34 +          sig \<times>			
    1.35 +          p_count"
    1.36  
    1.37  	(* operand stack *)
    1.38  	(* local variables *)
    1.39 @@ -29,22 +30,20 @@
    1.40  	(* program counter within frame *)
    1.41  
    1.42  
    1.43 -(** exceptions **)
    1.44 -
    1.45 +text {* exceptions: *}
    1.46  constdefs
    1.47 - raise_xcpt :: "bool => xcpt => xcpt option"
    1.48 -"raise_xcpt c x == (if c then Some x else None)"
    1.49 -
    1.50 -(** runtime state **)
    1.51 -
    1.52 -types
    1.53 - jvm_state = "xcpt option \\<times> aheap \\<times> frame list"	
    1.54 +  raise_xcpt :: "bool => xcpt => xcpt option"
    1.55 +  "raise_xcpt c x == (if c then Some x else None)"
    1.56  
    1.57  
    1.58 +text {* runtime state: *}
    1.59 +types
    1.60 +  jvm_state = "xcpt option \<times> aheap \<times> frame list"	
    1.61  
    1.62 -(** dynamic method lookup **)
    1.63  
    1.64 +text {* dynamic method lookup: *}
    1.65  constdefs
    1.66 - dyn_class	:: "'code prog \\<times> sig \\<times> cname => cname"
    1.67 -"dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
    1.68 +  dyn_class	:: "'code prog \<times> sig \<times> cname => cname"
    1.69 +  "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))"
    1.70 +
    1.71  end