Quellcode-Bibliothek Conclusion.thy

Sprache: Isabelle

(*<*)
―‹ ********************************************************************
* Project : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
* Version : 2.0
*
* Author : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
* (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
*
* This file : Conclusion
*
* Copyright (c) 2009 Université Paris-Sud, France
* Copyright (c) 2025 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‹Conclusion›

(*<*)
theory Conclusion
  imports "HOL-CSP"
begin
  (*>*)

section‹Related Work›
text‹As mentioned earlier, this work has its very ancient roots in a first formalization
A. Camilieri in the early 90s in HOL. This work was reformulated and substantially
in HOL-CSP 1.0 published in 1997. In 2005, Roggenbach and Isobe published
-Prover, a formal theory of a (fragment of) the Failures model of CSP. This work
to a couple of publications culminating in cite‹"IsobeRoggenbach2010"›; emphasis was put
actually completing the CSP theory up to the point where it is sufficiently tactically
to serve as a kind of tool. This theory is still maintained and last releases (the
one was released on 18 February 2019) can be
under 🪙‹https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html›. This theory
the first half of Roscoes theory of a Failures/Divergence model, i.e. the Failures part.
recently, Pasquale Noce
cite‹"Noninterference_CSP-AFP" and "Noninterference_Sequential_Composition-AFP" and
Noninterference_Concurrent_Composition-AFP"›
a theory of non interference notions based on an abstract denotational model fragment of
Failure/Divergence Model of CSP (without continuity and algebraic laws); this theory could
be rebuilt on top of our work.

present work could be another, more ``classic'' foundation of test-generation techniques
this kind paving the way to an interaction with FDR and its possibility to generate
transition systems as output that could drive specialized tactics in HOL-CSP 2.0.
›

section‹Lessons learned›
text‹We have ported a first formalization in Isabelle/HOL on the Failure/Divergence model of CSP,
with Isabelle93-7 in 1997, to a modern Isabelle version. Particularly,
use the modern declarative proof style available in Isabelle/Isar instead of imperative proof
, the latter being used in the old version. On the one hand, it is worth noting that some of
old theories still have a surprisingly high value: Actually it took time to develop the right
of abstraction in lemmas, which is thus still quite helpful and valuable to reconstruct
theory in the new version. If a substantially large body of lemmas is available, the degree of
tends to increase. On the other hand, redevelopment from scratch is unavoidable in parts
basic libraries change. For example, this was a necessary consequence of our decision to base
-CSP 2.0 on HOLCF instead of continuing the development of an older fixed-point theory; nearly
continuity proofs had to be redeveloped. Moreover, a fresh look on old proof-obligations
incite unexpected generalizations and some newly proved lemmas that cannot be constructed in
old version even with several attempts. The influence of the chosen strategy (from scratch
refactoring) on the proof length is inconclusive.

that our data does not allow to make a prediction on the length of a porting project ---
effort was distributed over a too long period and performed by a team with initially very
knowledge about CSP and interactive theorem proving.

is also worth noting that the restructuring of the theory, as well as the proofs
declarative Isar style), has substantially increased the possibility to parallelize
proof checking process and makes the entire theory more maintainable.

, having the entire theory formalized makes extensions such as parametized ticks
since the effect of changes of basic definitions can be traced consequently.
is an important aspect that extensions of this kind are not ad hoc and do not endanger
consistency.
›

section‹A Summary on New Results›
text‹Compared to the original version of HOL-CSP 1.0, the present theory is complete relative to
's Bookcite‹"roscoe:csp:1998"›. It contains a number of new theorems and some interesting
and unexpected) generalizations:
🪙 @{thm mono_Hiding} is now also valid for the infinite case (arbitrary hide-set A).
🪙 term‹P \ (A ∪ B) = (P \ A) \ B› is true for term‹finite A› (see @{thm Hiding_Un});
this was not even proven in HOL-CSP 1.0 for the singleton case! It can be considered as the
most complex theorem of this theory.
🪙 distribution laws of const‹Hiding› over const‹Sync› @{thm Hiding_Sync};
however, this works only in the finite case. A true monster proof.
🪙 distribution of const‹Mprefix› over const‹Sync› @{thm Mprefix_Sync_Mprefix} in the most
generalized case. Also a true monster proof, but reworked using symmetries and
abstractions to be more reasonable (and faster)
🪙 the synchronization operator is associative @{thm "Sync_assoc"}.
(In HOL-CSP 1.0, this had only be shown for special cases like @{thm Sync_assoc[where S = ‹UNIV›]}).
🪙 the generalized non deterministic prefix choice operator --- relevant for proofs of deadlock-freeness ---
has been added to the theory @{thm "Mndetprefix_def"}; it is proven monotone and
continuous @{thm Mndetprefix_cont} in the general case
(in contrast to the global choice without prefix, see @{thm GlobalNdet_cont}).
This is relevant for the definition of the deadlock reference processes @{thm DF_def} and @{thm "DF_S_K_I_P_{S_def}"}.
🪙 since Isabelle-2025, new support for read term‹c?a∈A → P a› and non deterministic write
term‹c!!a∈A → P a› has been added. Also, sliding choice has been added and new algebraic
laws involving this operator (see @{thm Hiding_Mprefix_non_disjoint}) have been proven.
›

(*<*)
end
  (*>*)

Messung V0.5 in Prozent

¤ 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.0.11Bemerkung: (vorverarbeitet am 2026-06-10) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.