equal
deleted
inserted
replaced
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))" |