🚀 go-pugleaf

In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes:


>Z will never emerge as a useful tool for real-world programmers and
>analysts because it cannot be expressed on glass tty's.

>Back to the drawing board and come up with an unambiguous syntax
>expressible in the intersection of the ASCII and EBCDIC codes
>and we can make some progress.

>We just don't have the time to muck with Troff or Latex just to write
>down our specs for the systems.  Also we'd like to see the specs online.

>Is this too much to ask?

No, it's not too much to ask !

After all, how long does it take to do something in latex ?
Ans: Close to forever.

The real world just won't stand still while you go and 'latex' the specs.

But then again, how often do you end up with software that doesn't meet its
specification. Or worse yet, according to the USERS it isn't what they
wanted.

Specification languages like Z may result (altough ALL software should have
some form of specification, even if it's in ENGLISH) in a project taking 
longer to complete overall BUT at the end of the day you will HAVE software 
which meets its spec. since Z (or whatever you choose to use) states 
PRECISELY what is required, no IFS or BUTS about it. 

So the extra (?) time spent writing the spec. in Z (or whatever) will
probably pay dividends during the lifetime of the software since you
not only have software which does what it's meant to but in case of 
future modifications to it, the Z specs also serve as documentation.

I also believe there is some kind of Z editor somewhere here at the 
University of Qld

Anyone from University of QLD care to comment ?


Yep, I think thats just about my $0.02 worth for today.

Writing for TRUTH, JUSTICE and CRUELTY (but mainly cruelty),

*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*

EMAIL: thomo@cs.uq.oz.au 			Ph: (07) 365 2726

SNAIL: John Thomas,         	               +------------------+
       c/o Computer Science Department,        |   And remember,  |
       University of Queensland,               | A HONKED nose is |
       Queensland, 4072 Australia. 	       |  a HAPPY nose !  |
                            	               +------------------+
*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*

In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes:

>Back to the drawing board and come up with an unambiguous syntax
>expressible in the intersection of the ASCII and EBCDIC codes
>and we can make some progress.

>We just don't have the time to muck with Troff or Latex just to write
>down our specs for the systems.  Also we'd like to see the specs online.

How about a graphics-based Z editor under SunView or X/Windows?  There are
people here at UQ working on such a beast and it's quite trendy.  You can
mix explanatory text, Z specs and even code if you like.  But it's still
coming along at the moment.

ASCII and EBCDIC terminals are quickly going the way of the dinosaur with
graphics terminals, high-resolution PC's, etc, becoming more common-place.
As for sending such specs through the mail, etc, the new mail format
Internet Draft specifies how you can send images, TeX documents, etc
through the mail and have them intelligently processed and displayed at
the other end, so that's not a problem either anymore.  (Given a year or
two for the mail and news readers to be updated :-).

As this progresses you won't need to think in ASCII or EBCDIC anymore, but
documents, so Z will fit in no worries with the emerging editors and
mail processing standards.  Think of writing a Z spec (or any spec for that
matter) as being an exercise in desktop publishing.

Cheers,

Rhys.

+=====================+==================================+
||  Rhys Weatherley   |  The University of Queensland,  ||
||  rhys@cs.uq.oz.au  |  Australia.  G'day!!            ||
||       "I'm a FAQ nut - what's your problem?"         ||
+=====================+==================================+

In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes:


>Z will never emerge as a useful tool for real-world programmers and
>analysts because it cannot be expressed on glass tty's.

Oh?	\begin{schema}{table}
	   data : Key \ffun Value		\\
	   keys : \fset Key			\\
	\ST
	   \dom data = keys
	\end{schema}				
	
	:-) :-)

Seriously though, using the fuzz or oz macros with LaTeX, Z is not all
that unreadable.  It is also not to difficult to come up with ascii
`lookalikes' for many of the symbols in the standard library; I often
use such approximations when sending questions involving Z text by mail.
e.g.
	\dom	==> dom
	\tfun	==> ->
	\pfun	==> +>
	\ffun	==> ++>
	\dres	==> <|
	\limg	==> (|
	etc

Perhaps someone has proposed a a standard set of these?
The variety of box notations is more of a problem, but perhaps you could
use just the latex \begin{...} and \end{...} delimiters?

>Back to the drawing board and come up with an unambiguous syntax
>expressible in the intersection of the ASCII and EBCDIC codes
>and we can make some progress.

Whats ambiguous about the syntax?  There are several type checkers available
for Z (for example, `Fuzz' by Mike Spivey at the PRG, Oxford Uni); there is
also a syntax-based editor at UQ -- all of which need a precise syntax on
which to work!

>We just don't have the time to muck with Troff or Latex just to write
>down our specs for the systems.  Also we'd like to see the specs online.

Do you mean you don't have time to install/learn LaTeX, or you find it
too difficult to write Z specs *in* LaTeX; is the latter, have you looked
at the macro packages zed.sty and oz.sty?

>Is this too much to ask?

IMHO, the concise notation is one of the attractions of Z, and part of the
attraction is the use of standard mathematical symbols -- yes, there are
some peculiar to Z, but I did not find them hard to learn once you note
their regularity.  Replacing these with ascii equivalents may help those
with acess only to ascii terminals, but I don't think that this would
suddenly make it more popular or accessible.


>----------------------
>	Brad Sherman (bks@alfa.berkeley.edu)

David Duke.

david@cs.uq.oz.au

In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes:


>>Back to the drawing board and come up with an unambiguous syntax
>>expressible in the intersection of the ASCII and EBCDIC codes
>>and we can make some progress.

In <2232@uqcspe.cs.uq.oz.au> david@cs.uq.oz.au (David Duke) writes:
>Whats ambiguous about the syntax?  There are several type checkers available
>for Z (for example, `Fuzz' by Mike Spivey at the PRG, Oxford Uni); there is
>also a syntax-based editor at UQ -- all of which need a precise syntax on
>which to work!

I am afraid this is not much of an argument. Both these parsers use a
restricted Z grammar. Yes I know Spivey's is "definitive", but it is still
a re-engineering of the language and is much more restrictive than what
people used to write down before there was an official syntax. The UQ
grammar (and it seems the Spivey one) is a linearised version of Z. This
means that you either have to put in more brackets than you would like,
or you must define precedents between operators that cannot interfer
semantically, such as + and union or more importantly function
application and function application.

An expression like

	f g a

can generally only mean one thing, either

	f : (X -> Y) -> (A -> B)
	g : X -> Y
	a : A
	f g a = (f(g))(a) : B
					example: f^3 x
or

	f : Y -> Z
	g : X -> Y
	a : X
	f g a = f(g(a)) : Z
					example: sin cos x

If either meaning is clear from the context, then the parser should
chose the right one regardless of precedent information. You should not
have to put brackets in to "force" the parser to read it the right way.

If neither meaning is clear from the context, for example an expression
involving type conformant expressions such as

	{} {} {}

then your really do have an ambiguity and it should be flagged as such
and not hidden by magical precedent applications.
--
Brendan Mahony                   | brendan@batserver.cs.uq.oz       
Department of Computer Science   | heretic: someone who disgrees with you
University of Queensland         | about something neither of you knows
Australia                        | anything about.