(*<*)
―‹ ********************************************************************
* Project : CSP-RefTK - A Refinement Toolkit for HOL-CSP
* Version : 1.0
*
* Author : Burkhart Wolff, Safouan Taha, Lina Ye.
*
* This file : An Introduction
*
* Copyright (c) 2020 Université Paris-Saclay, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************› (*>*)
chapter‹Context› (*<*) theory Introduction imports HOLCF begin (*>*)
section‹Introduction›
text‹
Sequential Processes CSP is a language
specify and verify patterns of interaction of concurrent systems.
with CCS and LOTOS, it belongs to the family of 🪙‹process algebras›.
's rich theory comprises denotational, operational and algebraic semantic facets
has influenced programming languages such as Limbo, Crystal, Clojure and
notably Golang @{cite "donovan2015go"}. CSP has been applied in
as a tool for specifying and verifying the concurrent aspects of hardware
, such as the T9000 transputer @{cite "Barret95"}.
theory of CSP, in particular the denotational Failure/Divergence Denotational Semantics,
been initially proposed in the book by Tony Hoare @{cite "Hoare:1985:CSP:3921"}, but evolved
since @{cite "BrookesHR84" and "brookes-roscoe85" and "roscoe:csp:1998"}.
of CSP properties has been centered around the notion of 🪙‹process refinement orderings›,
notably ‹_⊑FD_› and ‹_⊑_›. The latter turns the denotational domain of CSP into a Scott cpo
{cite "scott:cpo:1972"}, which yields semantics for the fixed point operator ‹μx. f(x)› provided ‹f› is continuous with respect to ‹_⊑_›. Since it is possible to express deadlock-freeness and
-freeness as a refinement problem, the verification of properties has been reduced
to a model-checking problem for a finite set of events ‹A›.
are interested in verification techniques for arbitrary event sets ‹A› or arbitrarily
processes. Such processes can be used to model dense-timed processes, processes
dynamic thread creation, and processes with unbounded thread-local variables and buffers.
may even be higher-order objects such as functions or again processes, paving the way
the modeling of re-programmable compute servers or dynamic distributed computing architectures.
, this adds substantial complexity to the process theory: when it comes to study the
of different denotational models, refinement-orderings, and side-conditions for
, paper-and-pencil proofs easily reach their limits of precision.
attempts have been undertaken to develop the formal theory of CSP in an interactive proof system,
in Isabelle/HOL @{cite "Camilleri91" and "tej.ea:corrected:1997" and "IsobeRoggenbach2010"}.
work is based on the most recent instance in this line, HOL-CSP 2.0, which has been published
AFP submission @{cite "HOL-CSP-AFP"} and whose development is hosted at 🪙‹https://gitlri.lri.fr/burkhart.wolff/hol-csp2.0›.
present AFP Module is an add-on on this work and develops some support for 🪙 example of induction schemes (mutual fixed-point Induction, K-induction), 🪙 a theory of explicit state normalisation which allows for proofs over certain
communicating networks of arbitrary size.
newpage ›
(* \<^enum> bridge-Lemmas between the classical refinement relations in the FD-semantics,
which allow for reduced refinement proof complexity in certain cases, and *)
section‹The Global Architecture of CSP\_RefTk› text‹
begin{figure}[ht] \centering \includegraphics[width=0.60\textwidth]{session_graph.pdf} \caption{The overall architecture: HOLCF, HOL-CSP, and CSP\_RefTk} \label{fig:fig1}
end{figure} ›
text‹The global architecture of CSP\_RefTk is shown in \autoref{fig:fig1}.
entire package resides on: 🪙session‹HOL-Eisbach› from the Isabelle/HOL distribution, 🪙session‹HOLCF› from the Isabelle/HOL distribution, and 🪙session‹HOL-CSP› 2.0 from the Isabelle Archive of Formal Proofs. ›
(* \<^noindent>Thetheories\<^verbatim>\<open>Assertion_ext\<close>and\<^verbatim>\<open>Fixind_ext\<close>areextensionsofthe
corresponding theories in \<^session>\<open>HOL-CSP\<close>. *)
(*<*) end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
