CSP-Prover/history

AIST and Swansea University
last updated 2023.08.03
[ Isobe > CSP-Prover > history ]
History
  • (11/06/2013) CSP-Prover Ver.5.1 for Isabelle 2013 was released on 6 June 2013. The definitions, lemmas, and theorems are the same as CSP-Prover Ver.5.1 for Isabelle 2012.
  • (17/11/2012) CSP-Prover Ver.5.1 for Isabelle 2012 was released on 17 November 2012. The definitions, lemmas, and theorems are the same as CSP-Prover Ver.5.1 for Isabelle 2011.
  • (02/04/2011) CSP-Prover Ver.5.1 for Isabelle 2011 was released on 2 April 2011. The definitions, lemmas, and theorems are the same as CSP-Prover Ver.5.1 for Isabelle 2009-2.
  • (26/10/2010) CSP-Prover Ver.5.1 for Isabelle 2009-2 was released on 26 October 2010. The definitions, lemmas, and theorems are the same as CSP-Prover Ver.5.1 for Isabelle 2009-1, but some notations were changed in accordance with Isabelle 2009-2 syntax. For example, "axclass" was replaced by "class" for declaring classes like cpo and cms.
  • (06/01/2010) CSP-Prover Ver.5.1 for Isabelle 2009-1 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 User-Guide-5-1.
    • The concatenation operator of traces "^^" is replaced by "^^^" for avoiding ambiguity because "^^" is used as the power function's symbol in Isabelle 2009-1.
  • (23/07/2009) CSP-Prover Ver.5.0 for Isabelle 2009 was released on 23 July 2009. The main differences from version 4 are summarized as follows:
    • The CSP semi-automatic proof commands are implemented as Isabelle-methods instead of ML-functions. See the last paragraph in Section 8.3 of the User-Guide-5-0.
    • Convenient 2 notations (<-->, <==>) for renaming are introduced and auxiliary laws for them are added to CSP-proof commands. See the last paragraph in Section 7.1 of the User-Guide-5-0.
  • (03/11/2008) Uniform Candy Distribution Puzzle (test version) for Isabelle 2008 was published on 03 November 2008.
  • (30/06/2008) CSP-Prover Ver.4.0 for Isabelle 2008 was released on 30 June 2008.
    • CSP-Prover Ver.4.0 is now available for Isabelle 2005, 2007, and 2008. See here.
    • In this version, the definitions on X-symbols of CSP-processes are separated from main theory files for avoiding a lot of warnings. (see here)
  • (18/02/2008) CSP-Prover Ver.4.0 for Isabelle 2007 was released on 18 February 2008.
    • CSP-Prover 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 CSP-Prover Ver.4.1 and a case study by Uniform Candy Distribution Puzzle were published on 22 January 2008.
  • (28/08/2007) CSP-Prover Ver.4.0 was released on 28 August 2007.
    • The most important difference from the previous version (CSP-Prover-3-0) 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 CSP-Prover-3.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 CSP-Prover2005), 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 CSP-Prover was published on 4 April 2007.
  • (10/05/2006) CSP-Prover Ver.3.0, which includes theorems for a complete axiom system, was released on 10 May 2006. The differences from previous version (CSP-Prover2005-2) are summarized as follows:
    • New CSP-laws were added, and the completeness of CSP-laws 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 stable-failures domain.
    • Single recursive operator MU, (replicated) alphabetized parallel operator, depth-restriction 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