🚀 go-pugleaf

In article <JIM.DAVIES.92Aug18151551@pierrot.prg.ox.ac.uk>,
Jim.Davies@prg.ox.ac.uk (A Wooden Fish on Wheels) writes:

|>In article <...> hallam@zeus02.desy.de (Phillip M. Hallam-Baker) writes:
|>
|>   If you are looking for a useful calculus then it might be a good idea to
|>   start by observing that both CSP and Z are already pretty complex
|>   systems. 
|>
|>I disagree.  
|>
|>The Z notation is simpler than any other formal method I can think of.
|>
|>The theory of CSP isn't that difficult to understand. 

That is precisely why they are useful.

|>Didn't someone like Einstein say that a theory should be "as simple as
|>possible, but no simpler"?  What's the use of switching to an easier 
|>calculus or method if it's no longer adequate?

I did not mean to imply go off and invent your own version of CSP and Z! However
in combining them you do not want to end up with something vastly more complex.


|>   Combining them is asking to produce something so mind boggling
|>   huge and vast that most people will move to something rather smaller of
|>   their own devising.
|>
|>It's the "divising" part that's the complicated bit.  I'm (reasonably) happy
|>to rely upon the skills of aircraft engineers when I fly; I don't expect to
|>build my own plane.  And that's more complicated than booking a ticket and
|>flying.  It's a bit of a useless analogy, but I'm sure you get the point. 

Yep, about as usless as my own analogy...!

What I was trying to get across was that if the cost of getting a workable
system together is having to live in a subset of CSP/Z then this is quite a
reasonable price to pay.


|>Just because we had to think in metric spaces in order to check that the
|>language and models of CSP were all hunky dory, it doesn't mean that you need
|>to know anything more than basic set theory in order to use them.  I'm sure
|>that a similar argument applies to Z...

But whence Z+CSP? It's one think to glue the two theories together with sticky
tape, quite another to do something usefull with the result. 

Occam accepts a set of simplifying assumtions which reduce the power of CSP but
create a useable system.

I would prefe to use an approach where I use the power of CSP to define an
implementation paradigm (eg a transaction processor) and then use Z to specify
at a different level of abstraction (eg the transactions themselves).

In other words I regard Jim not as a purveyor of motor cars but as a supplyer of
parts... yep you are right it is a useless analogy...

A better analogy might be to the use of design rules for silicon. I may take my
design rules and use them to demonstrate that a standard cell library is
correct, thereafter I use the standard cell library without looking under the
covers too often...

--

Phill Hallam-Baker