From RM@RSRE Wed Feb 19 13:07:52 1986
Via:        rlxa    ; 19 Feb 1986 13:05:10-WET
To: Z
From: Ruaridh Macdonald (on UK.MOD.RSRE) <RM@RSRE>
Date:    Wed, 19 Feb 86 13:04 GMT
Message-Id: <19 FEB 1986 13:04:25 RM@RSRE>
Subject: Z Forum, Volume 1 Issue 1
Acknowledge-To: RM@RSRE


21st January 1986              Z FORUM                  Volume 1 Issue 1
 
     This  is  what  I  hope  will  be  just  the  first  of a series of
discussion messages which will be distributed  round  the  community  of
developers  and users of the Z specification language.  Inevitably as we
get used to using Z we shall have thoughts on what we have learned about
how  best  to  use  it,  how  we  feel  it might usefully be extended or
amended, what implications  it  has  for  the  software  (and  hardware)
development  process,  and  such  issues.   Many of us will have queries
which we feel other people may be able to make  useful  comments  about,
and such thoughts could be bounced around in a forum like this.

     I shall be happy to receive contributions from you, to collect them
together and to send them out to all who would like to receive them.  If
you  know  of  other people who would like to see the Z Forum, or if you
are reading this message second hand and would like  to  receive  copies
yourself,  let  me  have the necessary electronic mail address to add to
the distribution list.  Since not everyone who may be  interested  in  Z
has  access to the Alvey Mail, we may wish to consider sending copies by
paper mail as well.

     The topics covered by this forum will, of  course,  depend  on  the
contributions sent in, but to start the ball rolling:

1. As a specification language, Z aims to enable the specifier to describe
   WHAT his system is expected to do, without having to worry about saying
   HOW the system will carry out its functions. However, when we come to
   refine our specifications to include more detail, we shall want to
   specify the algorithms which will be used by the implementation. Does
   Z require new constructs, such as WHILE DO, for example, in order to
   specify these algorithms adequately?
 
2. Suppose we are constructing a machine-readable form of Z. Should it be
   possible to determine the order in which functions are to be applied
   purely from the syntax, without having to check the types of the functions?
   For example

        a : A;      c : C;
        f : A -> B;         g : B -> C;
        h : (A -> B) -> (C -> D);
 
        Should we expect the machine reader to use type-checking to deduce
   that
         gfa  means  g(fa),
   while
         hfc  means  (hf)c  ?
 
3. Should we endeavour to make the proof process sufficiently simple that
   most programmers come to use specification and verification as a matter
   of course? Is it possible? If so, how?
 
Let's hear YOUR opinions on these and other topics.
 
The mailing list for the Z Forum is currently:
 
Susan Stepney          Marconi Research Centre
Ib Sorensen            Programming Research Group, Oxford University
Bernard Sufrin                              "
Nigel Haigh            Racal Information Technology Developments
Andrew Ricketts                          "
Trevor King            Royal Signals and Radar Establishment
Ruaridh Macdonald                        "
Colin O'Halloran                         "
Chris Sennett                            "
John McDermid          Systems Designers
 
******************** END OF Z FORUM ******************************

Ruaridh Macdonald (RM@RSRE)
Tel. Malvern (06845) 2733 Ext 3846