Theory Introduction

(*<*)
―‹ ********************************************************************
 * 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‹
Communicating Sequential Processes CSP is a language 
to specify and verify patterns of interaction of concurrent systems.
Together with CCS and LOTOS, it belongs to the family of ∗‹process algebras›. 
CSP's rich theory comprises denotational, operational and algebraic semantic facets 
and has influenced programming languages such as Limbo, Crystal, Clojure and
most notably Golang @{cite "donovan2015go"}. CSP has been applied in 
industry as a tool for specifying and verifying the concurrent aspects of hardware 
systems, such as the T9000 transputer @{cite "Barret95"}. 

The theory of CSP, in particular the denotational Failure/Divergence Denotational Semantics,
has been initially proposed in the book by Tony Hoare @{cite "Hoare:1985:CSP:3921"}, but evolved
substantially since @{cite "BrookesHR84" and "brookes-roscoe85" and "roscoe:csp:1998"}.

Verification of CSP properties has been centered around the notion of ∗‹process refinement orderings›,
most notably ‹_⊑⇩F⇩D_› 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 
that ‹f› is continuous with respect to ‹_⊑_›. Since it is possible to express deadlock-freeness and 
livelock-freeness as a refinement problem, the verification of properties has been reduced 
traditionally to a model-checking problem for a finite set of events ‹A›.

We are interested in verification techniques for arbitrary event sets ‹A› or arbitrarily 
parameterized processes. Such processes can be used to model dense-timed processes, processes 
with dynamic thread creation, and processes with unbounded thread-local variables and buffers.
Events may even be higher-order objects such as functions or again processes, paving the way
for the modeling of re-programmable compute servers or dynamic distributed computing architectures.
However, this adds substantial complexity to the process theory: when it comes to study the 
interplay of different denotational models, refinement-orderings, and side-conditions for 
continuity, paper-and-pencil proofs easily reach their limits of precision. 

Several attempts have been undertaken to develop the formal theory of CSP in an interactive proof system, 
mostly in Isabelle/HOL @{cite "Camilleri91" and "tej.ea:corrected:1997" and  "IsobeRoggenbach2010"}. 
This work is based on the most recent instance in this line, HOL-CSP 2.0, which has been published 
as AFP submission  @{cite "HOL-CSP-AFP"} and whose development is hosted at 
🌐‹https://gitlri.lri.fr/burkhart.wolff/hol-csp2.0›. 

The 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
›

(* ▸ 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]{figures/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}.
The 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.
›

(* 
⇤ The theories ▩‹Assertion_ext› and ▩‹Fixind_ext› are extensions of the 
corresponding theories in \<^session>‹HOL-CSP›. *)


(*<*)
end
  (*>*)