isabelle: src/HOL/MicroJava/JVM/JVMState.thy@82f68fd05094 (annotated)

8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/MicroJava/JVM/JVMState.thy
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	2	ID: $Id$
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	Author: Cornelia Pusch
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	4	Copyright 1999 Technische Universitaet Muenchen
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	5	*)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	6
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	7
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	8	header {* State of the JVM *}
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	9
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	10
10922 f1209aff9517 Store.thy is obsolete (newref isn't used any more) kleing parents: 10057 diff changeset	11	theory JVMState = Conform:
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	12
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	13
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	14	text {* frame stack :*}
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	15	types
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	16	opstack = "val list"
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	17	locvars = "val list"
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	18	p_count = nat
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	19
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	20	frame = "opstack \<times>
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	21	locvars \<times>
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	22	cname \<times>
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	23	sig \<times>
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	24	p_count"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	25
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	26	(* operand stack *)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	27	(* local variables *)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	28	(* name of def. class defined *)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	29	(* meth name+param_desc *)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	30	(* program counter within frame *)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	31
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	32
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	33	text {* exceptions: *}
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	34	constdefs
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	35	raise_xcpt :: "bool => xcpt => xcpt option"
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	36	"raise_xcpt c x == (if c then Some x else None)"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	37
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	38
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	39	text {* runtime state: *}
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	40	types
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	41	jvm_state = "xcpt option \<times> aheap \<times> frame list"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	42
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	43	end

author	wenzelm
	Tue, 23 Oct 2001 22:52:31 +0200
changeset 11908	82f68fd05094
parent 11177	749fd046002f
child 12519	a955fe2879ba
permissions	-rw-r--r--