|
8011
|
1 |
(* Title: HOL/MicroJava/JVM/Store.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Cornelia Pusch
|
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
|
5 |
|
|
|
6 |
The store.
|
|
|
7 |
|
|
|
8 |
The JVM builds on many notions already defined in Java.
|
|
|
9 |
Conform provides notions for the type safety proof of the Bytecode Verifier.
|
|
|
10 |
*)
|
|
|
11 |
|
|
|
12 |
Store = Conform +
|
|
|
13 |
|
|
|
14 |
syntax
|
|
|
15 |
value :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ \\<And> _")
|
|
|
16 |
translations
|
|
|
17 |
"t \\<And> x" == "the (t x)"
|
|
|
18 |
|
|
|
19 |
constdefs
|
|
|
20 |
newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
|
|
|
21 |
"newref s \\<equiv> \\<epsilon>v. s v = None"
|
|
|
22 |
|
|
|
23 |
end
|