Relay-Version: version B 2.10.2 9/18/84 +2.11; site uk.ac.ox.prgv
Posting-Version: version B 2.10.3 uknet 86/05/14; site uk.ac.oxford.prg
Path: prgv!mkhadmin
From: Ruaridh Macdonald (on UK.MOD.RSRE) <RM@uk.mod.rsre>
Newsgroups: zforum
Subject: Z Forum Issue 3.7
Message-ID: <08 NOV 1988 10:58:54 RM@RSRE>
Date: 8 Nov 88 11:55:25 GMT
Date-Received: 8 Nov 88 11:57:03 GMT
Lines: 387


 
8th November 1988              Z FORUM               Volume 3 Issue 7     
-----------------              -------               ----------------
 
                            Today's Topics
                            --------------
 
                          Z Reference Manual
                          Z Users' Meeting
 
---------------------------------------------------------------------
 
Date:    Thu, 3 Nov 88 16:13:08 GMT
From:    Mike Spivey <mike@uk.ac.oxford.prg>
Subject: Z Reference Manual

"The Z notation: a reference manual" by J.M. Spivey, published by
Prentice-Hall International in red-and-white soft covers is now
available at all good bookshops.  The price is about 17 pounds.

Thank you to the many people who helped me complete this project,
especially the members of the Z group at Oxford whose names appear on
the title-page.

-- Mike.

---------------------------------------------------------------------
 
Date:    Mon, 7 Nov 88 14:59:23 GMT
From: Jonathan Bowen <bowen@uk.ac.oxford.prg>
Subject: Z Tutorial, Workshop & User Meeting

Here is an electronic copy of a brochure which we are sending out to
our mailing list. At the end, a registration form is included which
may be printed, completed and returned to the organising secretary
if desired.


                OXFORD UNIVERSITY COMPUTING LABORATORY
                      PROGRAMMING RESEARCH GROUP


                              Z Tutorial,
                              Z Workshop
                                  and
                              3rd annual
                            Z Users Meeting



                       15th - 16th December 1988
                             to be held in

                                OXFORD

                                                                        Page 1

                              Z Tutorials
                Oxford University Computing Laboratory
                             Lecture Room
                             11 Keble Road
                        Thursday, 15th December
                   9.30am-12.30pm and 2.00pm-5.30pm


Audience:  The tutorials  are aimed at programmers,  software engineers,
analysts and managers of software development groups.  A basic knowledge
of Z (e.g. attendance at last year's Z Tutorial) is assumed.

Logicians and semanticists are not invited to apply!


Cost:  60,  including  course materials  but not including  lunch.  (The
tutors will be only too happy to recommend local places to eat!)

                         ____________________


Do you feel queasy when you see this?

          If $pre1 \Rightarrow pre2$ then $w:[pre1,post]
                  \sqsubseteq w:[pre2,post]$
          If $pre \wedge post2 \Rightarrow post1$ then
                  $w:[pre,post1] \sqsubseteq w:[pre,post2]$
          $w:[pre \wedge (\bigvee i \spot G_i), post]
                  = {\bf if}~ (\Alt i \spot G_i \rightarrow
                         w:[pre \wedge G_i, post]~{\bf fi}$
          $w:[I,I\wedge\neg(\bigvee i \spot G_i)] \sqsubseteq
                   {\bf do}~(\Alt i \spot G_i \rightarrow
                   w:[I \wedge G_i, I \wedge 0\leq V'<V])~{\bf od}$


                          Morning Tutorial on
                     Basic Concepts of Refinement
                            9.30am-12.30pm
                        Tutor:  Kitt Cowlishaw


If mathematical logic is not your native language,  then you are invited
to attend  this  half-day  tutorial.  It is designed  to make  the  most
important   mathematical   laws   of   refinement   crystal   clear   to
non-mathematicians.

By lunchtime you will have a clear understanding of:

  * The refinement relation

  * The w:[pre,post] notation for specification statements

  * Weakening the precondition

  * Strengthening the postcondition

                                                                        Page 2

  1   n \leq biggestsize \; Free                           [hypothesis]
  2   n \leq \# ( firstbiggest \; Free )      [1 size of first biggest]
  3   \# ( n \unlhd ( firstbiggest \; Free ) ) = n
                                              [2 size of initial slice]
  4   ( n \unlhd ( firstbiggest \; Free ) ) \subseteq
         ( firstbiggest \; Free )        [2 inclusion of initial slice]
  5   ( firstbiggest \; Free ) \subseteq Free
                                           [inclusion of first biggest]
  6   ( n \unlhd ( firstbiggest \; Free ) ) \subseteq Free
                                      [4,5 transitivity of $\subseteq$]
  7   ( n \unlhd ( firstbiggest \; Free ) ) \in Contig
                                          [contiguity of first biggest]
  8   \# ( n \unlhd ( firstbiggest \; Free ) ) = n
         ( n \unlhd ( firstbiggest \; Free ) ) \subseteq Free
         ( n \unlhd ( firstbiggest \; Free ) ) \in Contig
                                           [3,6,7 $\land$-introduction]
  9   \exists s: \power Addr \spot
         \# s = n \land s \subseteq Free \land s  \in Contig
                                             [8 $\exists$-introduction]


                         Afternoon Tutorial on
                      Proof and Z Specifications
                             2.00pm-5:30pm
                         Tutor:  Jim Woodcock


   ``To use mathematics without doing any proofs is to have all the
     illusion of formality, without any of its benefits.''

   ``Good specifications are distinguished from poor ones by the
     presence of proofs.''

   ``We improve by proving.''


If you have had some experience  in using Z for the formal specification
of software  systems,  but you don't do proofs  routinely,  then you are
invited  to  attend  this  half-day  tutorial.  It  is designed  to make
perfectly  clear to non-mathematicians  exactly  what proof  obligations
there are in a Z specification,  and how they can be discharged.  By the
time the pubs# open you will have a clear understanding of

  *  The initialisation theorem.

  *  The calculation of preconditions.

  *  How to state system properties.

You will  also  have  had some  exercise  in using  two important  proof
techniques  to  discharge  these  obligations:   natural  deduction  and
equational  reasoning.  An example of a real-life specification  will be
used as an illustration.


________________
# At least, those that have not taken advantage of the new legislation.

                                                                        Page 3

                              Z Workshop
                          Venue to be decided
                        Thursday, 15th December
                             9.30am-5.30pm



                     Z in the development process
                         a discussion workshop
                 Convener and Chairman:  John Nicholls


In  current  research  on  Software  Engineering,  there  is  increasing
emphasis  on studies of the development  process,  as can be seen by the
establishment  of  process  models  and  process  architectures.  The  Z
notation  is used in specification  and design,  but once a Z definition
(or other  formal  definition)  of a system  is available,  it can bring
benefits  to other  stages.  The aim of this  workshop  is therefore  to
consider the influence  of formal methods on the development  process as
a whole.

The meeting  will take the form of a short  introduction  to a topic  or
theme  by  a  leading  speaker,   followed   by  discussions   in  which
participants  will be invited  to raise  issues  and propose  ideas  and
directions for further work.

We will consider  how the use of formal methods  affects  the management
of software  projects,  and their  relationship  to other  parts  of the
development process, including:

  requirements
  user interface design
  documentation
  testing
  maintenance


Participants  at the meeting  should  have  experience  in working  with
formal methods in a development  project,  be planning  the introduction
of formal methods, or be interested in process studies.

Attendance  at the workshop will be by invitation,  but some places will
be available by application.  Please contact John Nicholls at the PRG if
you  would  like  to attend,  stating  the  topic(s)  in which  you  are
specially interested.


Cost:  20 pounds, including lunch.

                                                                        Page 4

                            Z Users Meeting
                    Department of External Studies
                             Rewley House
                          1 Wellington Square
                         Friday, 16th December
                             9.15am-5.30pm


This meeting provides an opportunity for Z users to meet each other,  to
hear  of recent  developments  in both  the  theoretical  and  practical
aspects of Z,  and to express their views about the directions of future
work.


                          Provisional agenda


      9.15 onwards          Registration, coffee
      9.30 -  9.45          Introduction
      9.45 - 10.15          Keynote speech by Martyn Thomas,
                                M.D. Praxis Systems plc
     10.15 - 11.00          Z standards, tools, education, etc.
     11.00 - 11.20          Coffee break
     11.20 - 13.00          Technical presentations
     13.00 - 14.30          Lunch and demonstrations
     14.30 - 16.00          Project presentations
     16.00 - 16.15          Break
     16.15 - 17.00          Project presentations
     17.00 - 17.30          Panel on the future of Z


Posters:  You are invited  to send or bring posters describing  research
related  to the use of Z.  These  will be displayed  at the meeting  and
will be included  in the distributed  notes  after the meeting.  Posters
should be A4 in size and provide a title, description,  and the name and
address of the author.


Cost:  40 pounds,  including lunch.  An information pack,  including a Z
bibliography,  will  be issued  to  each  participant  at  the  meeting.
Additionally,  each participant  will receive  a copy of the Proceedings
of the meeting together  with copy of posters  displayed  at the meeting
by post after the meeting.

                                                                        Page 5

                           Other information


We would  like  to draw your attention  if you are interested  in having
more  information  about  Z to  the  Z electronic  newsletter  called  Z
Forum.  Details  of this  may  be obtained  from  Mr.  Ruaridh Macdonald
(e-mail:   rm@uk.mod.rsre).   He expects to  be present  at the  meeting
and will be able to give you more information.

One of the very valuable functions  of the Z forum is to compile details
of all the current papers published and unpublished  which are available
in Z at the moment.  At the meeting a shorter list of references will be
handed out containing the most useful references.


Accommodation:  A number of rooms have been provisionally booked for the
Thursday night (15th December).  These will be held until 15th November.
If you are interested  in obtaining accommodation  please contact Joanna
Pulley as soon as possible,  and confirm your request IN WRITING by 15th
November.

Alternative  accommodation  booking service:  Oxford Information Centre,
telephone (0865) 726871.


Travel arrangements: Car parking is notoriously difficult in Oxford.  If
possible,  travel  by rail  (BR station  10-15  minutes  walk  to Rewley
House)  or coach  (Gloucester  Green  Coach  Station  5 minutes  walk to
Rewley House).



Programme committee:    Jonathan Bowen
                        John Nicholls
                        Jim Woodcock

Organising secretary:   Joanna Pulley

                        Programming Research Group
                        Oxford University Computing Laboratory
                        8-11 Keble Road
                        OXFORD  OX1 3QD

                        Tel:    (0865) 272568
                        Fax:    (0865) 272412  ATTN J.Pulley, COMLAB
                        E-mail: joanna@uk.ac.oxford.prg (JANET)
                          or    joanna@ox-prg.uucp
                                ...!uunet!mcvax!ukc!ox-prg!joanna (UUCP)


                OXFORD UNIVERSITY COMPUTING LABORATORY
                      PROGRAMMING RESEARCH GROUP

                           REGISTRATION FORM

                Z Tutorial, Workshop and Users Meeting
               Thursday 15th - Friday 16th December 1988

I wish  to  reserve  ..........  place(s)  for  the  Z Tutorial  on 15th
December at 60 pounds per place.

I would be interested in attending the Z Workshop on 15th December:

..........  place(s).

Topic(s) of interest at Z Workshop:  ...................................

(NOTE: the Z Tutorial and Workshop are concurrent  -  hence only one may
be attended by each individual.)

I require overnight accommodation for ..........  people on the night of
15th December.

I wish to reserve  ..........  place(s)  for the Z Users  Meeting  on
16th December at 40 pounds per place.

NAME(S) OF PARTICIPANT(S): .............................................

........................................................................

........................................................................

........................................................................

COMPANY/ORGANISATION: ..................................................

........................................................................

ADDRESS: ...............................................................

........................................................................

........................................................................

TELEPHONE: ........................ FAX: ...............................

E-MAIL: ........................... TELEX: .............................

I enclose a cheque for .......... / I will pay on arrival.

SIGNED: ........................... DATE: ..............................

Please return completed form to:

Joanna Pulley                           Tel:    (0865) 272568
Programming Research Group              Fax:    (0865) 272412
Oxford University Computing Laboratory            ATTN J.Pulley, COMLAB
8-11 Keble Road                         JANET:  joanna@uk.ac.oxford.prg
OXFORD  OX1 3QD                         UUCP:   joanna@ox-prg.uucp
                                                  ...!ukc!ox-prg!joanna

 
*************************** END OF Z FORUM 3.7 **********************