From 762680a20cbcc9f42c5c4dec1f0b9b465e50ce21 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Tue, 9 May 2023 20:18:33 +0200 Subject: [PATCH] eliminated calamity with tick symbol, layout imprivements, eliminated docitem --- Isabelle_DOF-Example-II/paper.thy | 51 +++++++++++++++---------------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/Isabelle_DOF-Example-II/paper.thy b/Isabelle_DOF-Example-II/paper.thy index 4902da4..932f386 100644 --- a/Isabelle_DOF-Example-II/paper.thy +++ b/Isabelle_DOF-Example-II/paper.thy @@ -77,9 +77,8 @@ be distinguished: \<^enum> the \<^emph>\external choice\, written \_\_\, which forces a process "to follow" whatever the environment offers, and \<^enum> the \<^emph>\internal choice\, written \_\_\, which imposes on the environment of a process - "to follow" the non-deterministic choices made. + "to follow" the non-deterministic choices made.\ -\ text\ Generalizations of these two operators \\x\A. P(x)\ and \\x\A. P(x)\ allow for modeling the concepts of \<^emph>\input\ and \<^emph>\output\: Based on the prefix operator \a\P\ (event \a\ happens, then the process @@ -127,10 +126,10 @@ attempt to formalize denotational \<^csp> semantics covering a part of Bill Rosc omitted.\}. \ -section*["pre"::tc,main_author="Some(@{docitem \bu\}::author)"] +section*["pre"::tc,main_author="Some(@{author \bu\}::author)"] \Preliminaries\ -subsection*[cspsemantics::tc, main_author="Some(@{docitem ''bu''})"]\Denotational \<^csp> Semantics\ +subsection*[cspsemantics::tc, main_author="Some(@{author ''bu''})"]\Denotational \<^csp> Semantics\ text\ The denotational semantics (following @{cite "roscoe:csp:1998"}) comes in three layers: the \<^emph>\trace model\, the \<^emph>\(stable) failures model\ and the \<^emph>\failure/divergence model\. @@ -190,7 +189,7 @@ of @{cite "IsobeRoggenbach2010"} is restricted to a variant of the failures mode \ -subsection*["isabelleHol"::tc, main_author="Some(@{docitem ''bu''})"]\Isabelle/HOL\ +subsection*["isabelleHol"::tc, main_author="Some(@{author ''bu''})"]\Isabelle/HOL\ text\ Nowadays, Isabelle/HOL is one of the major interactive theory development environments @{cite "nipkow.ea:isabelle:2002"}. HOL stands for Higher-Order Logic, a logic based on simply-typed \\\-calculus extended by parametric polymorphism and Haskell-like type-classes. @@ -219,10 +218,10 @@ domain theory for a particular type-class \\::pcpo\, \<^ie> fixed-point induction and other (automated) proof infrastructure. Isabelle's type-inference can automatically infer, for example, that if \\::pcpo\, then \(\ \ \)::pcpo\. \ -section*["csphol"::tc,main_author="Some(@{docitem ''bu''}::author)", level="Some 2"] +section*["csphol"::tc,main_author="Some(@{author ''bu''}::author)", level="Some 2"] \Formalising Denotational \<^csp> Semantics in HOL \ -subsection*["processinv"::tc, main_author="Some(@{docitem ''bu''})"] +subsection*["processinv"::tc, main_author="Some(@{author ''bu''})"] \Process Invariant and Process Type\ text\ First, we need a slight revision of the concept of \<^emph>\trace\: if \\\ is the type of the atomic events (represented by a type variable), then @@ -273,7 +272,7 @@ but this can be constructed in a straight-forward manner. Suitable definitions f \\\, \\\ and \\\ lifting \fst\ and \snd\ on the new \'\ process\-type allows to derive the above properties for any \P::'\ process\. \ -subsection*["operator"::tc, main_author="Some(@{docitem ''lina''})"] +subsection*["operator"::tc, main_author="Some(@{author ''lina''})"] \\<^csp> Operators over the Process Type\ text\ Now, the operators of \<^csp> \Skip\, \Stop\, \_\_\, \_\_\, \_\_\,\_\_\_\ etc. for internal choice, external choice, prefix and parallel composition, can @@ -298,7 +297,7 @@ The definitional presentation of the \<^csp> process operators according to @{ci follows always this scheme. This part of the theory comprises around 2000 loc. \ -subsection*["orderings"::tc, main_author="Some(@{docitem ''bu''})"] +subsection*["orderings"::tc, main_author="Some(@{author ''bu''})"] \Refinement Orderings\ text\ \<^csp> is centered around the idea of process refinement; many critical properties, @@ -328,7 +327,7 @@ states, from which no internal progress is possible. \ -subsection*["fixpoint"::tc, main_author="Some(@{docitem ''lina''})"] +subsection*["fixpoint"::tc, main_author="Some(@{author ''lina''})"] \Process Ordering and HOLCF\ text\ For any denotational semantics, the fixed point theory giving semantics to systems of recursive equations is considered as keystone. Its prerequisite is a complete partial ordering @@ -395,7 +394,7 @@ Fixed-point inductions are the main proof weapon in verifications, together with and the \<^csp> laws. Denotational arguments can be hidden as they are not needed in practical verifications. \ -subsection*["law"::tc, main_author="Some(@{docitem ''lina''})"] +subsection*["law"::tc, main_author="Some(@{author ''lina''})"] \\<^csp> Rules: Improved Proofs and New Results\ @@ -437,12 +436,12 @@ cases to be considered as well as their complexity makes pen and paper proofs practically infeasible. \ -section*["newResults"::tc,main_author="Some(@{docitem ''safouan''}::author)", - main_author="Some(@{docitem ''lina''}::author)", level= "Some 3"] +section*["newResults"::tc,main_author="Some(@{author ''safouan''}::author)", + main_author="Some(@{author ''lina''}::author)", level= "Some 3"] \Theoretical Results on Refinement\ text\\ -subsection*["adm"::tc,main_author="Some(@{docitem ''safouan''}::author)", - main_author="Some(@{docitem ''lina''}::author)"] +subsection*["adm"::tc,main_author="Some(@{author ''safouan''}::author)", + main_author="Some(@{author ''lina''}::author)"] \Decomposition Rules\ text\ In our framework, we implemented the pcpo process refinement together with the five refinement @@ -477,8 +476,8 @@ The failure and divergence projections of this operator are also interdependent, sequence operator. Hence, this operator is not monotonic with \\\<^sub>\\, \\\<^sub>\\ and \\\<^sub>\\, but monotonic when their combinations are considered. \ -subsection*["processes"::tc,main_author="Some(@{docitem ''safouan''}::author)", - main_author="Some(@{docitem ''lina''}::author)"] +subsection*["processes"::tc,main_author="Some(@{author ''safouan''}::author)", + main_author="Some(@{author ''lina''}::author)"] \Reference Processes and their Properties\ text\ We now present reference processes that exhibit basic behaviors, introduced in @@ -598,11 +597,11 @@ then it may still be livelock-free. % This makes sense since livelocks are worse \ -section*["advanced"::tc,main_author="Some(@{docitem ''safouan''}::author)",level="Some 3"] +section*["advanced"::tc,main_author="Some(@{author ''safouan''}::author)",level="Some 3"] \Advanced Verification Techniques\ text\ - Based on the refinement framework discussed in @{docitem "newResults"}, we will now + Based on the refinement framework discussed in @{technical "newResults"}, we will now turn to some more advanced proof principles, tactics and verification techniques. We will demonstrate them on two paradigmatic examples well-known in the \<^csp> literature: The CopyBuffer and Dijkstra's Dining Philosophers. In both cases, we will exploit @@ -613,7 +612,7 @@ verification. In the latter case, we present an approach to a verification of a architecture, in this case a ring-structure of arbitrary size. \ -subsection*["illustration"::tc,main_author="Some(@{docitem ''safouan''}::author)", level="Some 3"] +subsection*["illustration"::tc,main_author="Some(@{author ''safouan''}::author)", level="Some 3"] \The General CopyBuffer Example\ text\ We consider the paradigmatic copy buffer example @{cite "Hoare:1985:CSP:3921" and "Roscoe:UCS:2010"} @@ -661,7 +660,7 @@ of 2 lines proof-script involving the derived algebraic laws of \<^csp>. After proving that \SYSTEM\ implements \COPY\ for arbitrary alphabets, we aim to profit from this first established result to check which relations \SYSTEM\ has wrt. to the reference processes of -@{docitem "processes"}. Thus, we prove that \COPY\ is deadlock-free which implies livelock-free, +@{technical "processes"}. Thus, we prove that \COPY\ is deadlock-free which implies livelock-free, (proof by fixed-induction similar to \lemma: COPY \ SYSTEM\), from which we can immediately infer from transitivity that \SYSTEM\ is. Using refinement relations, we killed four birds with one stone as we proved the deadlock-freeness and the livelock-freeness for both \COPY\ and \SYSTEM\ processes. @@ -678,7 +677,7 @@ corollary deadlock_free COPY \ -subsection*["inductions"::tc,main_author="Some(@{docitem ''safouan''}::author)"] +subsection*["inductions"::tc,main_author="Some(@{author ''safouan''}::author)"] \New Fixed-Point Inductions\ text\ @@ -728,7 +727,7 @@ The astute reader may notice here that if the induction step is weakened (having the base steps require enforcement. \ -subsection*["norm"::tc,main_author="Some(@{docitem ''safouan''}::author)"] +subsection*["norm"::tc,main_author="Some(@{author ''safouan''}::author)"] \Normalization\ text\ Our framework can reason not only over infinite alphabets, but also over processes parameterized @@ -788,7 +787,7 @@ Summing up, our method consists of four stages: \ -subsection*["dining_philosophers"::tc,main_author="Some(@{docitem ''safouan''}::author)",level="Some 3"] +subsection*["dining_philosophers"::tc,main_author="Some(@{author ''safouan''}::author)",level="Some 3"] \Generalized Dining Philosophers\ text\ The dining philosophers problem is another paradigmatic example in the \<^csp> literature @@ -880,7 +879,7 @@ for a dozen of philosophers (on a usual machine) due to the exponential combinat Furthermore, our proof is fairly stable against modifications like adding non synchronized events like thinking or sitting down in contrast to model-checking techniques. \ -section*["relatedwork"::tc,main_author="Some(@{docitem ''lina''}::author)",level="Some 3"] +section*["relatedwork"::tc,main_author="Some(@{author ''lina''}::author)",level="Some 3"] \Related work\ text\ @@ -947,7 +946,7 @@ restrictions on the structure of components. None of our paradigmatic examples c be automatically proven with any of the discussed SMT techniques without restrictions. \ -section*["conclusion"::conclusion,main_author="Some(@{docitem ''bu''}::author)"]\Conclusion\ +section*["conclusion"::conclusion,main_author="Some(@{author ''bu''}::author)"]\Conclusion\ text\We presented a formalisation of the most comprehensive semantic model for \<^csp>, a 'classical' language for the specification and analysis of concurrent systems studied in a rich body of literature. For this purpose, we ported @{cite "tej.ea:corrected:1997"} to a modern version