|
1 (* Title: HOL/MicroJava/J/Conform.thy |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 |
|
6 Conformity relations for type safety of Java |
|
7 *) |
|
8 |
|
9 Conform = State + |
|
10 |
|
11 constdefs |
|
12 |
|
13 hext :: "aheap \\<Rightarrow> aheap \\<Rightarrow> bool" ( "_\\<le>|_" [51,51] 50) |
|
14 "h\\<le>|h' \\<equiv> \\<forall>a C fs. h a = Some(C,fs) \\<longrightarrow> (\\<exists>fs'. h' a = Some(C,fs'))" |
|
15 |
|
16 conf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> ty \\<Rightarrow> bool" ( "_,_\\<turnstile>_\\<Colon>\\<preceq>_" [51,51,51,51] 50) |
|
17 "G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<equiv> \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T" |
|
18 |
|
19 lconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> ('a \\<leadsto> val) \\<Rightarrow> ('a \\<leadsto> ty) \\<Rightarrow> bool" |
|
20 ("_,_\\<turnstile>_[\\<Colon>\\<preceq>]_" [51,51,51,51] 50) |
|
21 "G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts \\<equiv> \\<forall>n T. Ts n = Some T \\<longrightarrow> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T)" |
|
22 |
|
23 oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50) |
|
24 "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))" |
|
25 |
|
26 hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_,_\\<turnstile>\\<surd>" [51,51] 50) |
|
27 "G,h\\<turnstile>\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>" |
|
28 |
|
29 conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50) |
|
30 "s\\<Colon>\\<preceq>E \\<equiv> prg E,heap s\\<turnstile>\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E" |
|
31 |
|
32 end |