CoMet
Comparative Methodology
A Programming Methodology Project Proposal
For "history" please see last section: E-Mail Exchanges
Alloy: "Daniel Jackson" <dnj@mit.edu>,
CafeOBJ: "FUTATSUGI, Kokichi" <kokichi@jaist.ac.jp>,
Event B: "Michael J Butler" <mjb@ecs.soton.ac.uk>,
"Dominique Mery" <Dominique.Mery@loria.fr>,
RAISE: "Chris George" <cwg@iist.unu.edu>,
"Anne Haxthausen" <ah@imm.dtu.dk>,
"Jan Storbank Pedersen" <jnp@terma.com>,
"Dines Bjorner" <bjorner@gmail.com>,
VDM: "John Fitzgerald" <John.Fitzgerald@newcastle.ac.uk>,
"Peter Gorm Larsen" <pgl@iha.dk>,
Z: "Jim Woodcock" <Jim.Woodcock@cs.york.ac.uk>,
"Leo Freitag" leo@cs.york.ac.uk,
"Henson, Martin C" <hensm@essex.ac.uk>,
"Steve Reeves" <stever@cs.waikato.ac.nz>,
"Jonathan Bowen" <jpbowen@gmail.com>,
The current result is CoMet : Comparative Methodology, A Technical Note.
A Brief Overview of CafeOBJ/ProofScore and Formal
Lecture/Lab 1: Basics of CafeOBJ and Peano Style Natural Numbers
Lecture/Lab 2: Parametrized Modules and Generic List Structure
Lecture/Lab 3: Modeling and Specification of Mutual Exclusion Protocol (QLOCK) in OTS/CafeOBJ
Lecture/Lab 4: Proof Score Writing for QLOCK in OTS/CafeOBJ
Related Web Pages
We refer to a separate Web CoMet Repository document.
from Dines Bjorner <bjorner@gmail.com>
to Daniel Jackson <dnj@mit.edu>,
"FUTATSUGI, Kokichi" <kokichi@jaist.ac.jp>
Dominique Mery <Dominique.Mery@loria.fr>,
John Fitzgerald <John.Fitzgerald@newcastle.ac.uk>,
Peter Gorm Larsen <pgl@iha.dk>,
Jim Woodcock <Jim.Woodcock@cs.york.ac.uk>,
"Henson, Martin C" <hensm@essex.ac.uk>,
Steve Reeves <stever@cs.waikato.ac.nz>,,
Jonathan Bowen <jpbowen@gmail.com>
leo@cs.york.ac.uk
date 1 February 2010 15:19
subject "Formalisation-Parametrised" Lecture Notes (and Slides)
Dear Alloy Daniel,
CafeOBJ Kokichi,
Event B Dominique,
VDM John & Peter Gorm and
Z Jim & Leo, Martin & Steve,
Pls. find attached my latest set of lecture notes (+ slides):
35 pages covering principles of domain and requirements engineering,
53 pages covering their expression in the RAISE SL (RSL), and
35 pages covering a/the special topic of mereology.
Pls. note my lecture note paragraph on the middle of Page 3:
"Formalisation-Parametrised" Examples and Primer.
There I 'air' a proposal for a possibly joint project between yours
groups and me - aimed at providing the same small set of lecture
notes but, instead of suing RSL, using either of the Alloy. Event B,
VDM or Z SLs.
I am sure, should such an "exercise" emerge - that my narratives
of the examples (and even my formalisations) change (respectively
improve).
It would truly be an example of comparative schematology cum
specification ontology.
To a first approximation the "transliteration project" would
provide versions of all examples - notably their formalisations.
Then, undoubtedly some of the main text (of Chaps.1-5) would
have to be rephrased so as to fit "hand-in-glove" with all
the different SL instantiations.
All this, provided, you could/can more-or-less accept, as a basis,
the Domain to Requirements "transformation" proposition.
Sorry for intruding in, as I am sure, your busy and "other-priorities"
scheduled life.
Fondly yours
Dines
PS: My LaTeX lecture notes are set up as follows:
There are separate files for each sect. (sort of 'chapter').
And then there is a separate file for eeach of the very many examples.
In a first instantiation of a "transliteration" effort
* the example files need be 'transliterated' and
* a separate primer provided for Spec.Lang. SL (i.e., Appendix A)
PS: Should I also try ASM - and if so, whom ?
PS: Maybe I forgot to tell:
All the 53 examples of my notes are about the same
domain: transport net. Some could undoubtedly be
better examples.
Without the examples the
35 pages of sects.1-6 dwindle from to 20 pages
and the
87 pages of appendices A-B dwindle to 38 pages
dines
+++++++++++++++++++++++++++++
Prof., Dr Dines Bjørner, Dr.h.c., Emeritus
MAE, MRANS, ACM Fellow, IEEE Fellow
bjorner@gmail.com
http://www.imm.dtu.dk/~db
Fredsvej 11
DK-2840 Holte
Denmark
Phone: +45 4542 2141
+++++++++++++++++++++++++++++
from Jim Woodcock <jim@cs.york.ac.uk>
to Dines Bjorner <bjorner@gmail.com>
cc Daniel Jackson <dnj@mit.edu>,
Dominique Mery <Dominique.Mery@loria.fr>,
John Fitzgerald <John.Fitzgerald@newcastle.ac.uk>,
Peter Gorm Larsen <pgl@iha.dk>,
Jim Woodcock <Jim.Woodcock@cs.york.ac.uk>,
"Henson, Martin C" <hensm@essex.ac.uk>,
Steve Reeves <stever@cs.waikato.ac.nz>,,
Jonathan Bowen <jpbowen@gmail.com>
leo@cs.york.ac.uk
date 1 February 2010 15:29
subject Re: "Formalisation-Parametrised" Lecture Notes (and Slides)
Dines,
I'm very interested to contribute. Just recently, I've been
discussing the possibility of some common language to use with Alloy,
B, RAISE, VDM, Z, ... in order to exchange verification conditions
between different tools. Studying the same set of examples in these
different settings in a necessary prerequisite for that work. So
count me in.
Very best,
Jim
from Leo Freitas <leo@cs.york.ac.uk>
to Dines Bjorner <bjorner@gmail.com>
cc Daniel Jackson <dnj@mit.edu>,
Dominique Mery <Dominique.Mery@loria.fr>,
John Fitzgerald <John.Fitzgerald@newcastle.ac.uk>,
Peter Gorm Larsen <pgl@iha.dk>,
Jim Woodcock <Jim.Woodcock@cs.york.ac.uk>,
"Henson, Martin C" <hensm@essex.ac.uk>,
Steve Reeves <stever@cs.waikato.ac.nz>
date 1 February 2010 16:00
subject Re: "Formalisation-Parametrised" Lecture Notes (and Slides)
Dear Dines,
To have a common corpus like this is indeed very interesting.
And having similar / same examples worked out in various notations
will be great to compare different proof technologies / strategies.
As it happened with Mondex, I think we will have inter-notation
contributions and a very fertile exchange.
Let me know how I could help.
Best,
Leo
from Daniel Jackson <dnj@mit.edu>
to Dines Bjorner <bjorner@gmail.com>
cc Dominique Mery <Dominique.Mery@loria.fr>,
John Fitzgerald <John.Fitzgerald@newcastle.ac.uk>,
Peter Gorm Larsen <pgl@iha.dk>,
Jim Woodcock <Jim.Woodcock@cs.york.ac.uk>,
"Henson, Martin C" <hensm@essex.ac.uk>,
Steve Reeves <stever@cs.waikato.ac.nz>,,
Jonathan Bowen <jpbowen@gmail.com>
leo@cs.york.ac.uk
date 1 February 2010 16:31
Hi Dines,
I think this is a very good idea. I'm happy to participate. Two things
would make it easier to start with:
a. Is there a particular example we could focus on? The early
network/hubs/links example would be fine, but it would be good to
delineate it.
b. Are there some properties that are intended to follow from the
example that could be checked?
Daniel
from Dines Bjorner <bjorner@gmail.com>
to Daniel Jackson <dnj@mit.edu>
cc Dominique Mery <Dominique.Mery@loria.fr>,
John Fitzgerald <John.Fitzgerald@newcastle.ac.uk>,
Peter Gorm Larsen <pgl@iha.dk>,
Jim Woodcock <Jim.Woodcock@cs.york.ac.uk>,
"Henson, Martin C" <hensm@essex.ac.uk>,
Steve Reeves <stever@cs.waikato.ac.nz>,,
Jonathan Bowen <jpbowen@gmail.com>
leo@cs.york.ac.uk
date 1 February 2010 16:51
subject Re: "Formalisation-Parametrised" Lecture Notes (and Slides)
Dear Daniel,
Thanks most kindly for your forthcoming response.
Yes:
a: The one example is that which weaves its way from example 1 to and including
example 53 - being continuously expanded upon.
b: Indeed, you hit the, or rather, my "sore" nail: Yes, there are many
such properties to be ckecked "continuously" along the way - but
I have not mentioned any. And I do apologise. The reason is simple.
I wanted a tiny/small set of lecture notes for max. 3 weeks to cover
as many stages and steps (not of refinement, but) of specification:
domain and requirements. So I refrained from verification and model-
checking concerns. Also: I do believe that working out hopefully the
same example (in 53 "stages" !?) in at least 3, but hopefully al 5
SLs would teach us all something about what the various approaches
focus on wrt. verifiability/checkability and in this way we could set
up more general methodological guidelines etc. etc.
Fondly yours
Dines
from John Fitzgerald <john.fitzgerald@newcastle.ac.uk>
to Dines Bjorner <bjorner@gmail.com>,
Daniel Jackson <dnj@mit.edu>,
Dominique Mery <Dominique.Mery@loria.fr>,
Peter Gorm Larsen <pgl@iha.dk>,
Jim Woodcock <Jim.Woodcock@cs.york.ac.uk>,
"Henson, Martin C" <hensm@essex.ac.uk>,
Steve Reeves <stever@cs.waikato.ac.nz>,
"leo@cs.york.ac.uk" <leo@cs.york.ac.uk>,
Jonathan Bowen <jpbowen@gmail.com>
date 1 February 2010 17:39
subject RE: "Formalisation-Parametrised" Lecture Notes (and Slides)
Dear Dines
VDM is in :-) This will be a good way to increase the repertoire of
examples for all of the formalisms that we work with as well as
providing a good basis for comparison. We will also look to involve
other members of the VDM community so it's not just "the usual
suspects".
Warmest Regards
John & Peter
Dear Colleagues,
Pls.Note: I have added Michael Butler, Chris George, Anne
Haxthausen, Jan Storbank Pedersen and Jonathan Bowen
to the "original" mailing list. So far MB and
JB have OK'ed.
Pls. feel free to add further persons.
With John Fitzgerald, Chair of FME, we hope to open up
for -- invite -- a wider participation.
I have established a very tentative Web page: http://www.imm.dtu.dk/~db/comet
Pls. - until we have found a process whereby someone amongst us, perhaps
Jonathan Bowen ?, is trusted to take over and edit a "CoMet" web page, remark
directly to me - and, perhaps avoid CC to each and all ! I shall
faithfully and loyally incorporate your remarks.
Sincerely yours
Dines
Dear Dines, On Feb 1, 2010, at 10:51 AM, Dines Bjorner wrote: > > Dear Daniel, > > Thanks most kindly for your forthcoming response. > > Yes: > > a: The one example is that which weaves its way from example 1 to > and including example 53 - being continuously expanded upon. That's great, but I still think it may make sense to narrow it down. > > b: Indeed, you hit the, or rather, my "sore" nail: Yes, there are many > such properties to be ckecked "continuously" along the way - but > I have not mentioned any. And I do apologise. The reason is simple. > I wanted a tiny/small set of lecture notes for max. 3 weeks to cover > as many stages and steps (not of refinement, but) of specification: > domain and requirements. So I refrained from verification and model- > checking concerns. Also: I do believe that working out hopefully the > same example (in 53 "stages" !?) in at least 3, but hopefully al 5 > SLs would teach us all something about what the various approaches > focus on wrt. verifiability/checkability and in this way we could set > up more general methodological guidelines etc. etc. I understand that not mentioning tools or analyses makes sense. But in my view it's still worth recording intended properties as you go, as they're much harder to figure out later. They also provide a useful form of redundancy. I'm sure we'll be able to create some though, especially with your help. Daniel
Dear Daniel, Thanks for e-mail. I just broadcast one to you etc.: http://www2.imm.dtu.dk/~db/comet/. Sure, we need to focus on a few of the examples: http://www2.imm.dtu.dk/~db/comet/comet0.html#SECTION00060000000000000000 I suggest: some of the 4 + 8 initial ones. Yes, I will insert ' intended properties' as I go along editing these examples. Sincerely
/home/db/comet/comt0.tex
This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 -toc_depth 6 comet0
The translation was initiated by Dines Bjorner on 2010-06-26