author | kleing |
Thu, 21 Sep 2000 10:42:49 +0200 | |
changeset 10042 | 7164dc0d24d8 |
parent 9346 | 297dcbf64526 |
child 10061 | fe82134773dc |
permissions | -rw-r--r-- |
8011 | 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 |
||
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8082
diff
changeset
|
9 |
Conform = State + WellType + |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8082
diff
changeset
|
10 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8082
diff
changeset
|
11 |
types 'c env_ = "'c prog \\<times> (vname \\<leadsto> ty)" (* same as env of WellType.thy *) |
8011 | 12 |
|
13 |
constdefs |
|
14 |
||
10042 | 15 |
hext :: "aheap => aheap => bool" ( "_\\<le>|_" [51,51] 50) |
16 |
"h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))" |
|
8011 | 17 |
|
10042 | 18 |
conf :: "'c prog => aheap => val => ty => bool" ( "_,_\\<turnstile>_::\\<preceq>_" [51,51,51,51] 50) |
19 |
"G,h\\<turnstile>v::\\<preceq>T == \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T" |
|
8011 | 20 |
|
10042 | 21 |
lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool" |
22 |
("_,_\\<turnstile>_[::\\<preceq>]_" [51,51,51,51] 50) |
|
23 |
"G,h\\<turnstile>vs[::\\<preceq>]Ts == \\<forall>n T. Ts n = Some T --> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T)" |
|
8011 | 24 |
|
10042 | 25 |
oconf :: "'c prog => aheap => obj => bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50) |
26 |
"G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))" |
|
8011 | 27 |
|
10042 | 28 |
hconf :: "'c prog => aheap => bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50) |
29 |
"G\\<turnstile>h h\\<surd> == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>" |
|
8011 | 30 |
|
10042 | 31 |
conforms :: "state => java_mb env_ => bool" ("_::\\<preceq>_" [51,51] 50) |
32 |
"s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E" |
|
8011 | 33 |
|
34 |
end |