src/HOL/Bali/Trans.thy
author wenzelm
Mon, 25 Feb 2002 20:48:14 +0100
changeset 12937 0c4fd7529467
parent 12925 99131847fb93
child 13337 f75dfc606ac7
permissions -rw-r--r--
clarified syntax of ``long'' statements: fixes/assumes/shows;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Trans.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
12858
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
Operational transition (small-step) semantics of the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
execution of Java expressions and statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
PRELIMINARY!!!!!!!!
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    11
improvements over Java Specification 1.0 (cf. 15.11.4.4):
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    12
* dynamic method lookup does not need to check the return type
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    13
* throw raises a NullPointer exception if a null reference is given, and each
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    14
  throw of a system exception yield a fresh exception object (was not specified)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    15
* if there is not enough memory even to allocate an OutOfMemory exception,
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    16
  evaluation/execution fails, i.e. simply stops (was not specified)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    17
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    18
design issues:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    19
* Lit expressions and Skip statements are considered completely evaluated.
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    20
* the expr entry in rules is redundant in case of exceptions, but its full
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    21
  inclusion helps to make the rule structure independent of exception occurence.
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    22
* the rule format is such that the start state may contain an exception.
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    23
  ++ faciliates exception handling (to be added later)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    24
  +  symmetry
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    25
* the rules are defined carefully in order to be applicable even in not
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    26
  type-correct situations (yielding undefined values),
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    27
  e.g. the_Adr (Val (Bool b)) = arbitrary.
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    28
  ++ fewer rules 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    29
  -  less readable because of auxiliary functions like the_Adr
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    30
  Alternative: "defensive" evaluation throwing some InternalError exception
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    31
               in case of (impossible, for correct programs) type mismatches
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    32
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    33
simplifications:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    34
* just simple handling (i.e. propagation) of exceptions so far
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    35
* dynamic method lookup does not check return type (should not be necessary)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
Trans = Eval +
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
consts
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    41
  texpr_tstmt	:: "prog  (((expr  state)  (expr  state)) +
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    42
		            ((stmt  state)  (stmt  state))) set"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
syntax (symbols)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    45
  texpr :: "[prog, expr  state, expr  state]  bool "("__ 1 _"[61,82,82] 81)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    46
  tstmt :: "[prog, stmt  state, stmt  state]  bool "("__ 1 _"[61,82,82] 81)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    47
  Ref   :: "loc  expr"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    51
  "Ge_s 1 ex_s'" == "Inl (e_s, ex_s')  texpr_tstmt G"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    52
  "Gs_s 1 s'_s'" == "Inr (s_s, s'_s')  texpr_tstmt G"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
  "Ref a" == "Lit (Addr a)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    55
constdefs
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    56
  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    57
  sub_expr_expr :: "(expr  expr)  prop"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    58
  "sub_expr_expr ef  (G e s e' s'. G(   e,s) 1 (   e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    59
				     G(ef e,s) 1 (ef e',s'))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    60
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
inductive "texpr_tstmt G" intrs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
(* evaluation of expression *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
  (* cf. 15.5 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    65
  XcptE	"v. e  Lit v 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    66
				  G(e,Some xc,s) 1 (Lit arbitrary,Some xc,s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    68
 CastXX "PROP sub_expr_expr (Cast T)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    69
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    70
(*
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
  (* cf. 15.8.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    72
  NewC	"new_Addr (heap s) = Some (a,x);
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    73
	  s' = assign (hupd[ainit_Obj G C]s) (x,s) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    74
				G(NewC C,None,s) 1 (Ref a,s')"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
  (* cf. 15.9.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    77
(*NewA1	"sub_expr_expr (NewA T)"*)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    78
  NewA1	"G(e,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    79
			      G(New T[e],None,s) 1 (New T[e'],s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    80
  NewA	"i = the_Intg i'; new_Addr (heap s) = Some (a, x);
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    81
	  s' = assign (hupd[ainit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    82
			G(New T[Lit i'],None,s) 1 (Ref a,s')"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
  (* cf. 15.15 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    84
  Cast1	"G(e,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    85
			      G(Cast T e,None,s) 1 (Cast T e',s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    86
  Cast	"x'= raise_if (\<questiondown>G,sv fits T) ClassCast None 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    87
		        G(Cast T (Lit v),None,s) 1 (Lit v,x',s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
  (* cf. 15.7.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    90
(*Lit				"G(Lit v,None,s) 1 (Lit v,None,s)"*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
  (* cf. 15.13.1, 15.2 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    93
  LAcc	"v = the (locals s vn) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    94
			       G(LAcc vn,None,s) 1 (Lit v,None,s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
  (* cf. 15.25.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    97
  LAss1	"G(e,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    98
				 G(f vn:=e,None,s) 1 (vn:=e',s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    99
  LAss			    "G(f vn:=Lit v,None,s) 1 (Lit v,None,lupd[vnv]s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
  (* cf. 15.10.1, 15.2 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   102
  FAcc1	"G(e,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   103
			       G({T}e..fn,None,s) 1 ({T}e'..fn,s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   104
  FAcc	"v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T)) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   105
			  G({T}Lit a'..fn,None,s) 1 (Lit v,np a' None,s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
  (* cf. 15.25.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   108
  FAss1	"G(e1,None,s) 1 (e1',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   109
			  G(f ({T}e1..fn):=e2,None,s) 1 (f({T}e1'..fn):=e2,s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   110
  FAss2	"G(e2,np a' None,s) 1 (e2',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   111
		      G(f({T}Lit a'..fn):=e2,None,s) 1 (f({T}Lit a'..fn):=e2',s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   112
  FAss	"a = the_Addr a'; (c,fs) = the_Obj (heap s a);
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   113
	  s'= assign (hupd[aObj c (fs[(fn,T)v])]s) (None,s) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   114
		   G(f({T}Lit a'..fn):=Lit v,None,s) 1 (Lit v,s')"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
  (* cf. 15.12.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   121
  AAcc1	"G(e1,None,s) 1 (e1',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   122
				G(e1[e2],None,s) 1 (e1'[e2],s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   123
  AAcc2	"G(e2,None,s) 1 (e2',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   124
			    G(Lit a'[e2],None,s) 1 (Lit a'[e2'],s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   125
  AAcc	"vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   126
	  x' = raise_if (vo = None) IndOutBound (np a' None) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   127
			G(Lit a'[Lit i'],None,s) 1 (Lit (the vo),x',s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   131
  Call1	"G(e,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   132
			  G(e..mn({pT}p),None,s) 1 (e'..mn({pT}p),s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   133
  Call2	"G(p,None,s) 1 (p',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   134
		     G(Lit a'..mn({pT}p),None,s) 1 (Lit a'..mn({pT}p'),s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   135
  Call	"a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   136
 			   the (cmethd G (fst (the_Obj (h a))) (mn,pT)) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   137
	    G(Lit a'..mn({pT}Lit pv),None,(h,l)) 1 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   138
      (Body blk res l,np a' x,(h,init_vals lvars[Thisa'][Supera'][pnpv]))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   139
  Body1	"G(s0,None,s) 1 (s0',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   140
		   G(Body s0    e      l,None,s) 1 (Body s0'  e  l,s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   141
  Body2	"G(e ,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   142
		   G(Body Skip  e      l,None,s) 1 (Body Skip e' l,s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   143
  Body		  "G(Body Skip (Lit v) l,None,s) 1 (Lit v,None,(heap s,l))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
(* execution of statements *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
  (* cf. 14.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   148
  XcptS	"s0  Skip 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   149
				 G(s0,Some xc,s) 1 (Skip,Some xc,s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
  (* cf. 14.5 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   152
(*Skip	 			 "G(Skip,None,s) 1 (Skip,None,s)"*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
  (* cf. 14.2 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   155
  Comp1	"G(s1,None,s) 1 (s1',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   156
			       G(s1;; s2,None,s) 1 (s1';; s2,s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   157
  Comp			    "G(Skip;; s2,None,s) 1 (s2,None,s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
  (* cf. 14.7 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   165
  Expr1	"G(e ,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   166
				G(Expr e,None,s) 1 (Expr e',s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   167
  Expr			 "G(Expr (Lit v),None,s) 1 (Skip,None,s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
  (* cf. 14.8.2 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   170
  If1	"G(e ,None,s) 1 (e',s') 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   171
		      G(If(e) s1 Else s2,None,s) 1 (If(e') s1 Else s2,s')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   172
  If		 "G(If(Lit v) s1 Else s2,None,s) 1 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
		    (if the_Bool v then s1 else s2,None,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
  (* cf. 14.10, 14.10.1 *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   176
  Loop			  "G(While(e) s0,None,s) 1 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   178
*)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   179
  con_defs "[sub_expr_expr_def]"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
end