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!geraint
From: Ruaridh Macdonald (on UK.MOD.RSRE) <RM@uk.mod.rsre>
Newsgroups: zforum
Subject: Z Forum Issue 3.2
Message-ID: <19 <FEB 1988 15:21:44 RM@RSRE>
Date: 19 Feb 88 15:44:02 GMT
Date-Received: 19 Feb 88 15:45:24 GMT
Lines: 279


 
19th February 1988               Z FORUM                Volume 3 Issue 2
------------------               -------                ----------------
 
                              Today's Topics
                              --------------
 
                  Axiomatic Descriptions and Generic Definitions
                  Where Clauses
                  Z Archive at Oxford
                  Z Bibliography
                  Re. Brainteaser
 
----------------------------------------------------------------------
 
Date:    Fri, 22 Jan 88 12:11:34 GMT
From:    mike@uk.ac.oxford.prg
Subject: Axiomatic Descriptions and Generic Definitions

AXIOMATIC DESCRIPTIONS and GENERIC DEFINITIONS

by Mike Spivey

In this article, I discuss the similarities and differences between
the axiomatic description construct

	|  Declaration
	|--------
	|  Predicate

and the generic definition construct

	== [X] ============
	|  Declaration
	|--------
	|  Predicate
	------------------

In the reference manual, I have tried to sharpen and clarify the
differences between these two forms.

The axiomatic description box is used to introduce one or more
constants into the specification; their values may be constrained by the
predicate part, but they need not be completely fixed. For example,

	|  NoOfPrinters: nat
	|--------
	|  0 < NoOfPrinters <= 10

declares a new constant NoOfPrinters, a natural number, and constrains it
to have one of the values 1, 2, 3, 4, 5, 6, 7, 8, 9, 10.

In an implementation of the specification, NoOfPrinters will have to take
a single one of these values.  The informal text which surrounds the
mathematics should explain how the value is chosen: in this example, it
may be fixed when the system is installed on a new machine, and the
programmer must allow any of the 10 values to be chosen then.

Loosely-specified constants may also be used to name aspects of a system
which the programmer is free to choose: for example, the encoding of
directories as files in a filing system might be left to the programmer
to decide.  All the specification need say is that the encoding is a
total injection. Sometimes, the value of a constant may be fixed
by information outside the specification: the encoding of characters
as bytes, for example, is fixed by the hardware manufacturer, but the
details may be irrelevant to the specification.

The generic definition box introduces one or more generic constants into
the specification: it should be thought of as introducing some new
terminology, rather than naming part of the system being described.
The body of the definition must fix a single value for each constant
introduced, so that the terminology it introduces is unambiguous.
This means that the author of a specification must satisfy himself that
the predicates he writes have exactly one solution: this is a proof
obligation required to make sure the specification means anything at all.
In return for this restriction, the generic box may have generic parameters,
making it possible to introduce mathematical concepts without restricting
them to a single universe of values.

The value fixed by a generic definition may depend on the values taken
by constants introduced earlier by axiomatic definitions: for example,
in the definition

	== [X] ============
	|  printer_vec: P (seq X)
	|--------
	|  printer_vec = { s: seq X | #s = NoOfPrinters }
	------------------

which may be written more compactly as

	printer_vec[X]  ==  { s: seq X | #s = NoOfPrinters },

the length of a "printer vector" depends on the number of printers.

Why is the restriction to one value necessary?  I have already given
one reason -- that the terminology should be unambiguous -- and this
is related to the use which is made of generic boxes in the process
of specification.  But there are also strong technical reasons for
avoiding generic boxes which allow more than one value.  Let's explore
them with an example.

	== [X] ============
	|  left, right: X
	|--------			(WRONG)
	|  left /= right
	------------------

Here, two generic constants left and right are introduced, but the
only constraint is that left[X] and right[X] are different.  Three
problems have to be solved:

  1.	If X has only one element -- e.g. X = {0} -- then
	it's impossible to find two distinct members of X
	to be the values of left[X] and right[X].

  2.	If X is empty -- e.g. X = empty[Z] -- then it's
	impossible to find any members of X, different or
	not, to be the values of left[X] and right[X].

  3.	If left[Z] is used in two schemas which are then
	combined, can we assume that it has the same value
	in both?  Is left[N] the same as left[Z]? (Here, N and
	Z are the natural numbers and the integers).

This distinction between axiomatic and generic boxes came out of
my work on the semantics, and at first it seemed a little artificial.
But I now support the view that the two constructs correspond to two
different specification activities, and it is best to keep these two
activities separate.

The definition

	LHS[X]  ==  Expression

is a compact form of the generic definition

	== [X] ============
	|  LHS: T
	|--------
	|  LHS = Expression
	------------------

where T is the type of the expression on the right-hand side.
I have introduced the symbol == for these definitions to make the
distinction between them and one-line schema definitions unambiguous:
schemas are defined with the =^= symbol (an equal sign with a hat).
I think the two symbols =^= and equals-with-a-triangle are too similar
visually to avoid confusion, particularly for people new to Z. I
confess that I read == as "equals and will always equal"!

The left-hand side may have any of the following forms:

	ident[gen-params]			left[X]
	prefix-generic gen-param		seq X
	gen-param infix-generic gen-param	X --> Y

For completeness, I also allow e.g. (_ * _)[X] where * is an infix
function symbol, etc., but these look a bit odd, and a long definition
is easier to read.

----------------------------------------------------------------------
 
Date:    Thu, 21 Jan 88 18:48:31 GMT
From:    mike@uk.ac.oxford.prg
Subject: Where Clauses

WHERE CLAUSES

by Mike Spivey

Martin Weigele asks whether a name introduced by a where clause
in one schema is visible in another schema which imports it.

The answer is no.  A where clause is just a special kind of unique
quantifier:

	y = x + a where a = 3

means in effect

	exists_1 a: Z | a = 3 . y = x + a.

This means that variables introduced by a where clause are local to
the predicate in which the where clause appears. If the predicate
appears in the body of a schema, these variables do not become
components of the schema, and so they are not visible when the
schema is imported into another context.

In Martin Weigele's application, the names he wants to introduce
identify important concepts about his library database: the set of
books currently on loan, and the set of users of the library who
currently have at least one book.  These names will be useful, for
example, in stating the pre-conditions of operations on the database,
so they should be made into components of the state-space schema by
declaring them above the line.

----------------------------------------------------------------------
 
Date:    Wed, 10 Feb 88 09:58:16 GMT
From:    bowen@uk.ac.oxford.prg
Subject: Z archive at Oxford

There is now an archive server at Oxford which will allow people interested
in Z (and other things) to access Z-related files. In particular, back issues
of the Z FORUM electronic newsletter are available. To access the archive
server, send e-mail to:

	archive-server@uk.ac.oxford.prg			(on JANET)

The "Subject:" line and/or the body of the message may contain lines such as
the following:

	help			- help on using the archive server
	index			- general index of categories (e.g. "z")
	index z			- index of Z-related files
	send z 2.3 2.4		- send issues 2.3 and 2.4 of Z FORUM
	send z zbib		- send the Z bibliography
	path fred@somewhere	- specify return e-mail address (optional)

[The archive server does not appear to like 'index' and 'send' requests in
the same message. RM]

If you ask for a lot of files, or a lot of other people have asked for a lot
files, your message will be queued and sent when our machine has some free
time. If you ask for a small number of files, your request is likely to be
serviced more quickly. However, all being well, you should get the files
back within a day or two.

If you have serious problems accessing the archive and need human help, send
e-mail to:

	archive-management@uk.ac.oxford.prg

--
Jonathan Bowen
Programming Research Group
Oxford University

----------------------------------------------------------------------
 
From:    Ruaridh Macdonald (on UK.MOD.RSRE) <RM@RSRE>
Date:    Fri, 19 Feb 88 11:18    
Subject: Z Bibliography

     Note that the latest version of the Z Bibliography is now available
on request from the archive server.
 
----------------------------------------------------------------------
 
From:    Ruaridh Macdonald (on UK.MOD.RSRE) <RM@RSRE>
Date:    Fri, 19 Feb 88 11:20    
Subject: Re. Brainteaser

     Judging  from  conversations  I have had concerning the brainteaser
set in the last issue of the Forum, I did  not  perhaps  make  it  clear
enough that my particular interest was in a definition of the 'condense'
function which made it easy to prove that a 'partial condensation' of  a
sequence  condenses  to  the  same  result  as  condensing  the original
sequence.  I have seen and devised several different definitions of  the
condense  function,  and  have  two  proofs  of the theorem, but while a
number of the definitions appear quite neat, both of the proofs of  this
fairly 'obvious' theorem are long-winded and difficult to follow.

     The  point  of interest (and almost certainly painfully familiar to
those who have been involved with theorem  proving  for  any  length  of
time)  is  that  different,  but provably equivalent, definitions of the
same thing may make a great difference to the ease of proof of theorems.

     It is possible, of course, that as with the four colour theorem  to
take  a well-known example, no-one will be able to devise a simple proof
of the 'obvious' theorem - but if anyone can come up with a simple proof
of the theorem involving condensations, then I shall be delighted to see
it!


************************* END OF Z FORUM 3.2 *************************