| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/CSP_RefTK/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 6 kB |
|
Quelle Introduction.thySprache: Isabelle |
|||||||||||||||
|
(*<*) ―‹ ******************************************************************** * 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 S been initially proposed in the book by Tony Hoare @{cite "Hoare:1985:CSP:3921"} since @{cite "BrookesHR84" and "brookes-roscoe85" and "roscoe:csp:1998"}. of CSP properties has been centered around the notion of 🪙‹process refinement notably ‹_⊑FD_› and ‹_⊑_›. The latter turns the denotational domain of CSP into {cite "scott:cpo:1972"}, which yields semantics for the fixed point operator ‹μx. ‹f› is continuous with respect to ‹_⊑_›. Since it is possible to express deadlo -freeness as a refinement problem, the verification of properties has been reduc to a model-checking problem for a finite set of events ‹A›. are interested in verification techniques for arbitrary event sets ‹A› or arbit processes. Such processes can be used to model dense-timed processes, processes dynamic thread creation, and processes with unbounded thread-local variables an may even be higher-order objects such as functions or again processes, paving t the modeling of re-programmable compute servers or dynamic distributed computin , this adds substantial complexity to the process theory: when it comes to study 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 interac in Isabelle/HOL @{cite "Camilleri91" and "tej.ea:corrected:1997" and "IsobeRog work is based on the most recent instance in this line, HOL-CSP 2.0, which has 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> The theories \<^verbatim>\<open>Assertion_ext\<close> and \<^verbatim>\<open>Fixind_ corresponding theories in \<^session>\<open>HOL-CSP\<close>. *) (*<*) end (*>*)
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09