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