diff --git a/Isabelle_DOF-Example-II/document/preamble.tex b/Isabelle_DOF-Example-II/document/preamble.tex index 38c30447..0e10611a 100644 --- a/Isabelle_DOF-Example-II/document/preamble.tex +++ b/Isabelle_DOF-Example-II/document/preamble.tex @@ -1,6 +1,8 @@ %% This is a placeholder for user-specific configuration and packages. \usepackage{stmaryrd} +\usepackage{pifont}% http://ctan.org/pkg/pifont + \title{} \author{<AUTHOR>} diff --git a/Isabelle_DOF-Example-II/paper.thy b/Isabelle_DOF-Example-II/paper.thy index 61d6387b..4902da42 100644 --- a/Isabelle_DOF-Example-II/paper.thy +++ b/Isabelle_DOF-Example-II/paper.thy @@ -146,7 +146,7 @@ Note that the trace sets, representing all \<^emph>\<open>partial\<close> histor text*[ex1::math_example, status=semiformal, level="Some 1"] \<open> Let two processes be defined as follows: - \<^enum> \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close> + \<^enum> \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close> \<^enum> \<open>P\<^sub>n\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<sqinter> (b \<rightarrow> Stop)\<close> \<close> @@ -212,7 +212,7 @@ distribution comes with rich libraries comprising Sets, Numbers, Lists, etc. whi For this work, a particular library called \<^theory_text>\<open>HOLCF\<close> is intensively used. It provides classical domain theory for a particular type-class \<open>\<alpha>::pcpo\<close>, \<^ie> the class of types \<open>\<alpha>\<close> for which - \<^enum> a least element \<open>\<bottom>\<close> is defined, and + \<^enum> a least element \<open>\<bottom>\<close> is defined, and \<^enum> a complete partial order \<open>_\<sqsubseteq>_\<close> is defined. For these types, \<^theory_text>\<open>HOLCF\<close> provides a fixed-point operator \<open>\<mu>X. f X\<close> as well as the @@ -222,15 +222,13 @@ automatically infer, for example, that if \<open>\<alpha>::pcpo\<close>, then \< section*["csphol"::tc,main_author="Some(@{docitem ''bu''}::author)", level="Some 2"] \<open>Formalising Denotational \<^csp> Semantics in HOL \<close> -text\<open>\<close> - subsection*["processinv"::tc, main_author="Some(@{docitem ''bu''})"] \<open>Process Invariant and Process Type\<close> text\<open> First, we need a slight revision of the concept of \<^emph>\<open>trace\<close>: if \<open>\<Sigma>\<close> is the type of the atomic events (represented by a type variable), then -we need to extend this type by a special event \<open>\<surd>\<close> (called "tick") signaling termination. -Thus, traces have the type \<open>(\<Sigma>+\<surd>)\<^sup>*\<close>, written \<open>\<Sigma>\<^sup>\<surd>\<^sup>*\<close>; since \<open>\<surd>\<close> may only occur at the end of a trace, -we need to define a predicate \<open>front\<^sub>-tickFree t\<close> that requires from traces that \<open>\<surd>\<close> can only occur +we need to extend this type by a special event \<open>\<checkmark>\<close> (called "tick") signaling termination. +Thus, traces have the type \<open>(\<Sigma>\<uplus>\<checkmark>)\<^sup>*\<close>, written \<open>\<Sigma>\<^sup>\<checkmark>\<^sup>*\<close>; since \<open>\<checkmark>\<close> may only occur at the end of a trace, +we need to define a predicate \<open>front\<^sub>-tickFree t\<close> that requires from traces that \<open>\<checkmark>\<close> can only occur at the end. Second, in the traditional literature, the semantic domain is implicitly described by 9 "axioms" @@ -245,24 +243,24 @@ Informally, these are: \<^item> the tick accepted after a trace \<open>s\<close> implies that all other events are refused; \<^item> a divergence trace with any suffix is itself a divergence one \<^item> once a process has diverged, it can engage in or refuse any sequence of events. - \<^item> a trace ending with \<open>\<surd>\<close> belonging to divergence set implies that its - maximum prefix without \<open>\<surd>\<close> is also a divergent trace. + \<^item> a trace ending with \<open>\<checkmark>\<close> belonging to divergence set implies that its + maximum prefix without \<open>\<checkmark>\<close> is also a divergent trace. More formally, a process \<open>P\<close> of the type \<open>\<Sigma> process\<close> should have the following properties: -@{cartouche [display] \<open>([],{}) \<in> \<F> P \<and> +@{cartouche [display, indent=10] \<open>([],{}) \<in> \<F> P \<and> (\<forall> s X. (s,X) \<in> \<F> P \<longrightarrow> front_tickFree s) \<and> (\<forall> s t . (s@t,{}) \<in> \<F> P \<longrightarrow> (s,{}) \<in> \<F> P) \<and> (\<forall> s X Y. (s,Y) \<in> \<F> P \<and> X\<subseteq>Y \<longrightarrow> (s,X) \<in> \<F> P) \<and> (\<forall> s X Y. (s,X) \<in> \<F> P \<and> (\<forall>c \<in> Y. ((s@[c],{}) \<notin> \<F> P)) \<longrightarrow> (s,X \<union> Y) \<in> \<F> P) \<and> -(\<forall> s X. (s@[\<surd>],{}) \<in> \<F> P \<longrightarrow> (s,X-{\<surd>}) \<in> \<F> P) \<and> +(\<forall> s X. (s@[\<checkmark>],{}) \<in> \<F> P \<longrightarrow> (s,X-{\<checkmark>}) \<in> \<F> P) \<and> (\<forall> s t. s \<in> \<D> P \<and> tickFree s \<and> front_tickFree t \<longrightarrow> s@t \<in> \<D> P) \<and> (\<forall> s X. s \<in> \<D> P \<longrightarrow> (s,X) \<in> \<F> P) \<and> -(\<forall> s. s@[\<surd>] \<in> \<D> P \<longrightarrow> s \<in> \<D> P)\<close>} +(\<forall> s. s@[\<checkmark>] \<in> \<D> P \<longrightarrow> s \<in> \<D> P)\<close>} Our objective is to encapsulate this wishlist into a type constructed as a conservative theory extension in our theory \<^holcsp>. -Therefore third, we define a pre-type for processes \<open>\<Sigma> process\<^sub>0\<close> by \<open> \<P>(\<Sigma>\<^sup>\<surd>\<^sup>* \<times> \<P>(\<Sigma>\<^sup>\<surd>)) \<times> \<P>(\<Sigma>\<^sup>\<surd>)\<close>. +Therefore third, we define a pre-type for processes \<open>\<Sigma> process\<^sub>0\<close> by \<open> \<P>(\<Sigma>\<^sup>\<checkmark>\<^sup>* \<times> \<P>(\<Sigma>\<^sup>\<checkmark>)) \<times> \<P>(\<Sigma>\<^sup>\<checkmark>)\<close>. Forth, we turn our wishlist of "axioms" above into the definition of a predicate \<open>is_process P\<close> of type \<open>\<Sigma> process\<^sub>0 \<Rightarrow> bool\<close> deciding if its conditions are fulfilled. Since \<open>P\<close> is a pre-process, we replace \<open>\<F>\<close> by \<open>fst\<close> and \<open>\<D>\<close> by \<open>snd\<close> (the HOL projections into a pair). @@ -351,7 +349,7 @@ We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^su text\<open>The third condition \<open>\<psi>\<^sub>\<M>\<close> implies that the set of minimal divergent traces (ones with no proper prefix that is also a divergence) in \<open>P\<close>, denoted by \<open>Mins(\<D> P)\<close>, should be a subset of the trace set of \<open>Q\<close>. -%One may note that each element in \<open>Mins(\<D> P)\<close> do actually not contain the \<open>\<surd>\<close>, +%One may note that each element in \<open>Mins(\<D> P)\<close> do actually not contain the \<open>\<checkmark>\<close>, %which can be deduced from the process invariants described %in the precedent @{technical "processinv"}. This can be explained by the fact that we are not %really concerned with what a process does after it terminates. @@ -566,13 +564,13 @@ the Failure/Divergence Semantics of \<^csp>.\<close> Definition*[X10::"definition", level="Some 2"]\<open> \<open>deadlock\<^sub>-free P \<equiv> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close> \<close> -text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close> +text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<checkmark>\<close>, the union of \<open>\<checkmark>\<close> and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot be deadlocked after any non-terminating trace. \<close> Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>", level="Some 2"] -\<open> \<^hfill> \<^br> \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close> +\<open> \<^hfill> \<^br> \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<checkmark>}\<union>events_of P) \<notin> \<F> P)\<close> \<close> Definition*[X11, level="Some 2"]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<close> text\<open> Recall that all five reference processes are livelock-free.