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

8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/MicroJava/JVM/JVMState.thy
41589 bbd861837ebc tuned headers; wenzelm parents: 35416 diff changeset	2	Author: Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	*)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	4
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	5	chapter \<open>Java Virtual Machine \label{cha:jvm}\<close>
58886 8a6cac7c7247 modernized header; wenzelm parents: 42463 diff changeset	6
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	7	section \<open>State of the JVM\<close>
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	8
15860 a344c4284972 partial modernising of theory headers paulson parents: 13674 diff changeset	9	theory JVMState
a344c4284972 partial modernising of theory headers paulson parents: 13674 diff changeset	10	imports "../J/Conform"
a344c4284972 partial modernising of theory headers paulson parents: 13674 diff changeset	11	begin
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	12
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	13	subsection \<open>Frame Stack\<close>
42463 f270e3e18be5 modernized specifications; wenzelm parents: 41589 diff changeset	14	type_synonym opstack = "val list"
f270e3e18be5 modernized specifications; wenzelm parents: 41589 diff changeset	15	type_synonym locvars = "val list"
f270e3e18be5 modernized specifications; wenzelm parents: 41589 diff changeset	16	type_synonym p_count = nat
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	17
42463 f270e3e18be5 modernized specifications; wenzelm parents: 41589 diff changeset	18	type_synonym
12519 a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	19	frame = "opstack \<times>
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	20	locvars \<times>
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	21	cname \<times>
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	22	sig \<times>
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 10042 diff changeset	23	p_count"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	24
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61361 diff changeset	25	\<comment> "operand stack"
6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61361 diff changeset	26	\<comment> "local variables (including this pointer and method parameters)"
6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61361 diff changeset	27	\<comment> "name of class where current method is defined"
6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61361 diff changeset	28	\<comment> "method name + parameter types"
6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61361 diff changeset	29	\<comment> "program counter within frame"
12519 a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	30
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	31
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	32	subsection \<open>Exceptions\<close>
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15860 diff changeset	33	definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where
13674 f4c64597fb02 * empty log message * streckem parents: 13063 diff changeset	34	"raise_system_xcpt b x \<equiv> raise_if b x None"
12519 a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	35
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	36	subsection \<open>Runtime State\<close>
42463 f270e3e18be5 modernized specifications; wenzelm parents: 41589 diff changeset	37	type_synonym
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61361 diff changeset	38	jvm_state = "val option \<times> aheap \<times> frame list" \<comment> "exception flag, heap, frames"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	39
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	40
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	41	subsection \<open>Lemmas\<close>
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	42
12519 a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	43	lemma new_Addr_OutOfMemory:
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	44	"snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	45	proof -
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	46	obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	47	moreover
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	48	assume "snd (new_Addr hp) = Some xcp"
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	49	ultimately
a955fe2879ba exception merge + cleanup kleing parents: 11177 diff changeset	50	show ?thesis by (auto dest: new_AddrD)
13052 3bf41c474a88 canonical start state kleing parents: 12911 diff changeset	51	qed
3bf41c474a88 canonical start state kleing parents: 12911 diff changeset	52
13674 f4c64597fb02 * empty log message * streckem parents: 13063 diff changeset	53	end

author	wenzelm
	Tue, 09 Jan 2018 20:03:14 +0100
changeset 67394	b591933d39ec
parent 62042	6c6ccf573479
child 67443	3abf6a722518
permissions	-rw-r--r--