Theory Conclusion
chapter‹Conclusion›
theory Conclusion
imports Assertions
begin
section‹Related Work›
text‹As mentioned earlier, this work has its very ancient roots in a first formalization
of A. Camilieri in the early 90s in HOL. This work was reformulated and substantially
extended in HOL-CSP 1.0 published in 1997. In 2005, Roggenbach and Isobe published
CSP-Prover, a formal theory of a (fragment of) the Failures model of CSP. This work
led to a couple of publications culminating in @{cite "IsobeRoggenbach2010"}; emphasis was put
on actually completing the CSP theory up to the point where it is sufficiently tactically
supported to serve as a kind of tool. This theory is still maintained and last releases (the
latest one was released on 18 February 2019) can be
found under 🌐‹https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html›. This theory
represents the first half of Roscoes theory of a Failures/Divergence model, i.e. the Failures part.
More recently, Pasquale Noce
@{cite "Noninterference_CSP-AFP" and "Noninterference_Sequential_Composition-AFP" and
"Noninterference_Concurrent_Composition-AFP"}
developed a theory of non-interference notions based on an abstract denotational model fragment of
the Failure/Divergence Model of CSP (without continuity and algebraic laws); this theory could
probably be rebuilt on top of our work.
The present work could be another, more "classic" foundation of test-generation techniques
of this kind paving the way to an interaction with FDR and its possibility to generate
labelled 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,
done with Isabelle93-7 in 1997, to a modern Isabelle version. Particularly,
we use the modern declarative proof style available in Isabelle/Isar instead of imperative proof
one, the latter being used in the old version. On the one hand, it is worth noting that some of
the old theories still have a surprisingly high value: Actually it took time to develop the right
granularity of abstraction in lemmas, which is thus still quite helpful and valuable to reconstruct
the theory in the new version. If a substantially large body of lemmas is available, the degree of
automation tends to increase. On the other hand, redevelopment from scratch is unavoidable in parts
where basic libraries change. For example, this was a necessary consequence of our decision to base
HOL-CSP 2.0 on HOLCF instead of continuing the development of an older fixed-point theory; nearly
all continuity proofs had to be redeveloped. Moreover, a fresh look on old proof-obligations
may incite unexpected generalizations and some newly proved lemmas that cannot be constructed in
the old version even with several attempts. The influence of the chosen strategy (from scratch
or refactoring) on the proof length is inconclusive.
Note that our data does not allow to make a prediction on the length of a porting project ---
the effort was distributed over a too long period and performed by a team with initially very
different knowledge about CSP and interactive theorem proving.
›
section‹A Summary on New Results›
text‹Compared to the original version of HOL-CSP 1.0, the present theory is complete relative to
Roscoe's Book@{cite "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 hiding over synchronisation @{thm Hiding_Sync};
however, this works only in the finite case. A true monster proof.
▸ the synchronization operator is associative @{thm "Sync_assoc"}.
(In HOL-CSP 1.0, this had only be shown for special cases like @{thm "Par_assoc"}).
▸ the generalized non-deterministic choice operator --- relevant for proofs of deadlock-freeness ---
has been added to the theory @{thm "Mndetprefix_def"}; it is proven monotone in the general case and
continuous for the special case @{thm Mndetprefix_cont} relevant for the definition of the
deadlock reference processes @{thm DF_def} and @{thm "DF⇩S⇩K⇩I⇩P_def"}.›
end