This commit is contained in:
parent
697b4fddeb
commit
a6e62b30a9
|
@ -479,9 +479,10 @@ term " MODIFY VARS DO TRY \<langle>init\<rangle>\<^sub>a; body CATCH restore ;
|
|||
|
||||
section \<open>Hoare logic\<close>
|
||||
|
||||
definition hoare_aprog_t :: \<open>('s, 'e) abr upred \<Rightarrow> ('s, 'e) abr upred \<Rightarrow>
|
||||
term "((Abs_aprog o Abs_prog) ((P \<oplus>\<^sub>p \<Sigma>\<^sub>A\<^sub>B\<^sub>R) \<turnstile>\<^sub>n (\<lceil>(Q \<oplus>\<^sub>p \<Sigma>\<^sub>A\<^sub>B\<^sub>R) \<and> (A \<oplus>\<^sub>p abrupt)\<rceil>\<^sub>>)) \<sqsubseteq> PROG)"
|
||||
definition hoare_aprog_t :: \<open>'s upred \<Rightarrow> ('s) upred \<Rightarrow>
|
||||
'e option upred \<Rightarrow> ('s, 'e) aprog \<Rightarrow> bool\<close>
|
||||
where "hoare_aprog_t P Q A PROG =
|
||||
((Abs_aprog o Abs_prog) (P \<turnstile>\<^sub>n (\<lceil>Q\<rceil>\<^sub>> \<and> \<lceil>(A \<oplus>\<^sub>p abrupt)\<rceil>\<^sub>>)) \<sqsubseteq> PROG)"
|
||||
term \<open>hoare_aprog_t P Q ( \<guillemotleft>Some e\<guillemotright> =\<^sub>u D) THROW(e)\<close>
|
||||
((Abs_aprog o Abs_prog) ((P \<oplus>\<^sub>p \<Sigma>\<^sub>A\<^sub>B\<^sub>R) \<turnstile>\<^sub>n (\<lceil>(Q \<oplus>\<^sub>p \<Sigma>\<^sub>A\<^sub>B\<^sub>R) \<and> (A \<oplus>\<^sub>p abrupt)\<rceil>\<^sub>>)) \<sqsubseteq> PROG)"
|
||||
term \<open>hoare_aprog_t P (&x =\<^sub>u \<guillemotleft>1\<guillemotright>) (\<guillemotleft>e \<notin> REF\<guillemotright>) (THROW(e); x :== \<guillemotleft>1\<guillemotright>)\<close>
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue