[
Date Prev][
Date Next][
Thread Prev][
Thread Next][
Date Index][
Thread Index]
[
List Home]
|
Re: [stellation-res] Sorry for the
|
On Thursday, August 28, 2003, at 03:32 PM, Jonathan Gossage wrote:
----- Original Message -----
From: "Jim Wright - IBM Research" <jwright@xxxxxxxxxxxxxx>
To: <stellation-res@xxxxxxxxxxxxxxx>
Sent: Thursday, August 28, 2003 3:13 PM
Subject: Re: [stellation-res] Sorry for the
At 02:08 PM 8/28/2003, Jonathan Gossage wrote:
Subject: Re: [stellation-res] Sorry for the
More information about Z is available here:
http://www.zuser.org/z/
I tried the site several times but could get no response.
Odd..... I visited it this morning, but also cannot access it
presently.
I found the site by Googling on "Z specification language" and looking
for promising/recommended hits. There were some other
likely sites as well:
http://www.rbjones.com/rbjpub/cs/csfm03.htm
http://www.comlab.ox.ac.uk/archive/z.html
Both are accessible as I write this; the second (UK) site seems
to be particularly good.
Mark recommended this book to me:
The Way of Z: Practical Programming with Formal Methods, Jonathan
Jacky.
Cambridge University Press, 1997.
The book has a web site: http://staff.washington.edu/~jon/z-book/
I also found those sites with the exact same Google spec :-) but the
book
reference was what I was really looking for. Are you considering the
original Z or are you thinking of Object Z which I also found
references to
and which looks to be closer to what we might want to do.
I'm not a fan of object-Z. I think it's very misguided, for two reasons.
First - Z is already on the border of overcomplexity. Many people claim
that
it's no good because it's so expressive that it allows people to say
more than
they intend, and that their specs become invalid as a result. I don't
agree
with that, but I *do* see the complexity of Z as a problem, and as a
limit. Nothing
that adds to the semantics of Z without taking away in other areas is
clearly
putting itself beyond the line of too damned much complexity.
My other problem with things like OZ is that by moving closer to
implementation
abstractions, it loses much of the purpose of a specification distinct
from
an implementation.
The thing about formal specifications is that they are, by nature,
distant from implementation. And that distance is where much of their
value comes from.
Implementation may require all sorts of elaborate types, inheritance
relationships, and all manner of implementation tricks. But a formal
spec should have none of that - just the bare semantics.
When I wrote a Z spec for Stellation, it didn't really resemble the
implementation
very much at all. But it defined what the implementation *meant*; what
the
operations *should* do, without having to get bogged down in *how* it
worked.
So, for example, for a checkin, I could assert:
forall x in artifacts, version_history(x') \superseteq
version_history(x);
forall x not in changed_artifacts, version_history(x') =
version_history(x);
forall x in changed_artifacts, version_history(x') =
version_history(x) +
new_version(x)
That says nothing about how it worked. But it says what it means: after
a checkin,
version histories are unchanged or extended; for elements in the
changeset, the
history is extended by the new version; for elements outside the
changeset, the
history is unchanged.
What I was actually thinking about is that it's probably about time to
give the core
repository a good cleanup; a lot of cruft gradually migrated into it,
and I want to clean it out. And some of its semantics are going to
change, and I need to understand how. So
for the repository changed, I'm seriously thinking of two
possibilities: breaking out my
Z tools, and doing Z again; or trying out Dan Jackson's Alloy tool.
(Alloy is a very
nifty tool done by Dan's group at MIT. The language is, essentially, a
Z subset; but
it's got the ability to allow you to run tests: does this behavioral
specification correctly
make this error impossible? The language is much less expressive than Z
(which
is not necessarily a criticism; Z is rather overblown); but that power
reduction
enables much niftiness.)
-Mark
Regards
Jonathan
_______________________________________________
stellation-res mailing list
stellation-res@xxxxxxxxxxxxxxx
http://dev.eclipse.org/mailman/listinfo/stellation-res
Mark Craig Chu-Carroll, IBM T.J. Watson Research Center
*** The Stellation project: Advanced SCM Research
*** http://stellation.eclipse.org
*** Work: mcc@xxxxxxxxxxxxxx/Home: markcc@xxxxxxx
Mark Craig Chu-Carroll, IBM T.J. Watson Research Center
*** The Stellation project: Advanced SCM Research
*** http://stellation.eclipse.org
*** Work: mcc@xxxxxxxxxxxxxx/Home: markcc@xxxxxxx
