1(* 2 * Copyright 2017, Data61, CSIRO 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(DATA61_BSD) 9 *) 10 11theory CLanguage 12imports "CProof" 13begin 14 15definition 16 creturn :: "((c_exntype \<Rightarrow> c_exntype) \<Rightarrow> ('c, 'd) state_scheme \<Rightarrow> ('c, 'd) state_scheme) 17 \<Rightarrow> (('a \<Rightarrow> 'a) \<Rightarrow> ('c, 'd) state_scheme \<Rightarrow> ('c, 'd) state_scheme) 18 \<Rightarrow> (('c, 'd) state_scheme \<Rightarrow> 'a) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com" 19where 20 "creturn rtu xfu v \<equiv> (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);; (Basic (rtu (\<lambda>_. Return));; THROW))" 21 22definition 23 creturn_void :: "((c_exntype \<Rightarrow> c_exntype) \<Rightarrow> ('c, 'd) state_scheme 24 \<Rightarrow> ('c, 'd) state_scheme) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com" 25where 26 "creturn_void rtu \<equiv> (Basic (rtu (\<lambda>_. Return));; THROW)" 27 28definition 29 cbreak :: "((c_exntype \<Rightarrow> c_exntype) \<Rightarrow> ('c, 'd) state_scheme 30 \<Rightarrow> ('c, 'd) state_scheme) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com" 31where 32 "cbreak rtu \<equiv> (Basic (rtu (\<lambda>_. Break));; THROW)" 33 34definition 35 ccatchbrk :: "( ('c, 'd) state_scheme \<Rightarrow> c_exntype) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com" 36where 37 "ccatchbrk rt \<equiv> Cond {s. rt s = Break} SKIP THROW" 38 39definition 40 cchaos :: "('b \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a,'c,'d) com" 41where 42 "cchaos upd \<equiv> Spec { (s0,s) . \<exists>v. s = upd v s0 }" 43 44definition 45 "guarded_spec_body F R = Guard F (fst ` R) (Spec R)" 46 47end 48