src/HOL/Bali/Trans.thy
changeset 13688 a0b16d42d489
parent 13384 a34e38154413
child 14981 e73f8140af78
equal deleted inserted replaced
13687:22dce9134953 13688:a0b16d42d489
     1 (*  Title:      HOL/Bali/Trans.thy
     1 (*  Title:      HOL/Bali/Trans.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     David von Oheimb
     3     Author:     David von Oheimb and Norbert Schirmer
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     5 
     6 Operational transition (small-step) semantics of the 
     6 Operational transition (small-step) semantics of the 
     7 execution of Java expressions and statements
     7 execution of Java expressions and statements
     8 
     8 
   321 
   321 
   322   (* cf. 14.10, 14.10.1 *)
   322   (* cf. 14.10, 14.10.1 *)
   323 Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
   323 Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
   324         \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
   324         \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
   325 
   325 
   326 Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
   326 Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
   327 
   327 
   328 ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   328 ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   329          \<Longrightarrow>
   329          \<Longrightarrow>
   330          G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
   330          G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
   331 Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
   331 Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"