last updated 2023.08.03
[
Isobe >
CSPProver > history ]
History

(11/06/2013)
CSPProver Ver.5.1 for Isabelle 2013 was released on 6 June 2013.
The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 2012.

(17/11/2012)
CSPProver Ver.5.1 for Isabelle 2012 was released on 17 November 2012.
The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 2011.

(02/04/2011)
CSPProver Ver.5.1 for Isabelle 2011 was released on 2 April 2011.
The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 20092.

(26/10/2010) CSPProver Ver.5.1 for Isabelle 20092 was released on 26 October 2010.
The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 20091,
but some notations were changed in accordance with Isabelle 20092 syntax.
For example, "axclass" was replaced by "class" for declaring classes like cpo and cms.

(06/01/2010) CSPProver Ver.5.1 for Isabelle 20091 was released on 6 January 2010.
The definitions, lemmas, and theorems are the same as Ver.5.0 except that:

Convenient 3 notations (<, <<, <==) for renaming are defined and auxiliary laws
for them are proven. See the last paragraph in Section 7.1 of the UserGuide51.

The concatenation operator of traces "^^" is replaced by "^^^" for avoiding ambiguity
because "^^" is used as the power function's symbol in Isabelle 20091.

(23/07/2009) CSPProver Ver.5.0 for Isabelle 2009 was released on 23 July 2009.
The main differences from version 4 are summarized as follows:

The CSP semiautomatic proof commands are implemented as Isabellemethods
instead of MLfunctions. See the last paragraph in Section 8.3 of the UserGuide50.

Convenient 2 notations (<>, <==>) for renaming are introduced and auxiliary laws
for them are added to CSPproof commands. See the last paragraph in Section 7.1
of the UserGuide50.

(03/11/2008)
Uniform Candy Distribution Puzzle (test version) for Isabelle 2008 was published on 03 November 2008.

(30/06/2008) CSPProver Ver.4.0 for Isabelle 2008 was released on 30 June 2008.

CSPProver Ver.4.0 is now available for Isabelle 2005, 2007, and 2008. See here.

In this version, the definitions on Xsymbols of CSPprocesses are separated
from main theory files for avoiding a lot of warnings. (see here)

(18/02/2008) CSPProver Ver.4.0 for Isabelle 2007 was released on 18 February 2008.

CSPProver Ver.4.0 is now available for both Isabelle 2005 and Isabelle 2007. See here.

This version for Isabelle 2007 unexpectedly causes warnings such that
Currently parsed expression could be extremely ambiguous,
which does not happen in Isabelle 2005. We are now looking for the cause.

(22/01/2008) A test version of the developing CSPProver Ver.4.1 and
a case study by Uniform Candy Distribution Puzzle were published on 22 January 2008.

(28/08/2007) CSPProver Ver.4.0 was released on 28 August 2007.

The most important difference from the previous
version (CSPProver30) is that process names are
explicitly introduced in the basic syntax of the
version 4.0. We theoretically studied how recursions
can be expressed by replicated internal choices
instead of process names in CSPProver3.0, and then
we got some interesting results. However, we found
that it would be better to use process names for
expressing recursions more naturally. Process names
were introduced also in old versions (e.g
CSPProver2005), but they are expressed in a more
elegant style in the version 4.

(04/04/2007) A development snapshot (Ver.4.00) of the next version of CSPProver
was published on 4 April 2007.

(10/05/2006) CSPProver Ver.3.0, which includes theorems
for a complete axiom system, was released on 10 May
2006. The differences from previous version
(CSPProver20052) are summarized as follows:

New CSPlaws were added, and the completeness of CSPlaws was proven in a new package FNF_F.

The power of Replicated internal choice was
extended. It allowed our CSP dialect to be expressive
with respect to the stablefailures domain.

Single recursive operator MU, (replicated)
alphabetized parallel operator, depthrestriction
operator were added.

All the theory files were polished and reorganized to packages CSP, CSP_T, and CSP_F.

The expressions of recursive processes were improved in more elegant style.

etc