HDTenEightyP/NetNews huggingface dataset:
From: mjw@hpl.hewlett-packard.co.uk (Mike Wray)
Newsgroups: comp.specification.z
Subject: Re: Trees in Z (was: common data structures in Z
Date: 28 Jan 93 08:44:14 GMT
X-Mailer: mail-news 2.0.3


Continuing the discussion about generic free types,
it seems to me that they would be prefectly OK in Z because
they have a direct translation into existing Z.

At present we can define a tree of integers (using Z for the integers):


	ITREE = leaf<<Z>> | join<< Z X ITREE X ITREE>>

This stands for (more or less)

	[ITREE]

	[ leaf: Z -> ITREE; join: Z X ITREE X ITREE -> ITREE |
	  
	  your favourite axiomatisation of freely generated ]

and is a convenient shorthand for the axioms defining
freely generated.


A similar interpretation can be given to generic free types.
Consider a putative generic tree type:

	TREE[A] = leaf<<A>> | join<< A X TREE[A] X TREE[A]>>

with ITREE defined using it:

	ITREE = TREE[Z]

What does this mean? Consider the schema


 *- TREE[A, B] -----------------------------------------
 |
 | leaf: A -> B
 |
 | join: A X B X B -> B
 |
 +------------------------------------------------------
 |
 | leaf and join are bijections onto their ranges,
 | their ranges partition B,
 | B is the least set closed under join
 | (or any of the many equivalent closure properties)
 +------------------------------------------------------

We can now declare ITREE and assert the TREE property of it:

	[ITREE]

	TREE[Z, ITREE]

More generally, a generic free type


	Free[A] = f1<< Type1>> | .... | fn<< Typen>>

Corresponds to the schema

 *- Free[A, B] -----------------------------------------
 |
 | f1: Type1(B/Free[A]) -> B
 |
 | ...
 |
 | fn: Typen(B/Free[A]) -> B
 |
 +------------------------------------------------------
 | The fi are bijections onto their ranges,
 | the ranges partition B,
 | closure property (B is closed under any fj with B as 
 | an argument type)
 +------------------------------------------------------

 where Type1(B/Free[A]) means Type1 with B substituted for Free[A].


 An instance C = Free[D] corresponds to

	[C]
	Free[C,D]

Thus, we interpret a generic free type as a schema which can be
used to define instances.  Indeed, one can use this technique to
simulate generic free types in Z today.
The same technique extends to free types of more than one 
parameter, and is equivalent to the present semantics for
zero parameters.


Mike Wray

 
 +----------------------------------+-------------------------------------+
 |                                  |   Mike Wray                         |
 |     mjw@hplb.hpl.hp.co.uk        |   Hewlett-Packard Laboratories      |
 |     mjw@hplb.hpl.hp.com          |   Filton Road                       |
 |                                  |   Stoke Gifford                     |
 +----------------------------------+   Bristol        BS12 6QZ           |
 | Phone +44 272 228262 Direct      |   UK                                |
 |       +44 272 799910 Switchboard |                                     |
 +----------------------------------+-------------------------------------+
From: pky@fmg.bt.co.uk (Pete Young)
Newsgroups: comp.specification.z
Subject: Z font for Microsoft Word
Date: 27 Jan 93 14:01:00 GMT
Organization: British Telecom
X-Newsreader: Tin 1.1 PL5

Normally I'm perfectly happy to use the fuzz package to typeset and
print Z. However, I looks as though I will soon have to work out how
to include Z in Microsoft Word documents. 

I'd be very keen to hear from anyone who can give me information on any of the
following:

* The existance of any Z fonts for MS-Word

* How to define custom fonts for MS-Word

* How to convert postscript/tfm/pk/gf fonts to something that can be
  understood by MS-Word

* How to use LaTeX/dvi2ps (or any other TeX driver) to produce a  
  "schema-sized" chunk of output, rather than the page-sized lump
  that I currently get.

* How to hack a PostScript file to crop an image.

* Any other bright ideas on how this problem can be solved.

Email to pky@fmg.bt.co.uk please and I'll summarise.

Regards

Pete


-- 
  ____________________________________________________________________
  Pete Young        	  pky@fmg.bt.co.uk        Phone +44 473 227151
    "Most people prefer entertaining nonsense to unexciting reality"
From: kokichi@etl.go.jp (Kokichi Futatsugi)
Newsgroups: comp.specification.z
Subject: New Font Selection Scheme and fuzz.sty
Date: 28 Jan 93 02:45:31 GMT
Reply-To: futatsugi@etl.go.jp
X-Mailer: mail-news 2.0.3

Dear Dr. Mike Spivey,

you write:
 |Sender: zforum-request@prg.ox.ac.uk
 |Date: Fri, 6 Nov 92 12:17:51 GMT
 |From: Mike.Spivey@prg.ox.ac.uk
...
 |To obtain a (free) copy of the new fuzz.sty, or details of how to get
 |the fuzz package, which includes a type-checker for Z specifications
 |as well as a LaTeX style option and fonts for printing them, send
 |e-mail to mike@prg.oxford.ac.uk

Please let me know how to get "fuzz.sty" and related materials.  

Thanking you in advance,

Kokichi Futatsugi
Electrotechnical Laboratory (ETL) /
Japan Advanced Institute of Science and Technology (JAIST)
Address: ETL, 1-1-4 Umezono, Tsukuba Science City, Ibaraki 305, JAPAN
Tel:     +81 298 58 5163
Fax:     +81 298 58 5891
E-mail:  futatsugi@etl.go.jp
Newsgroups: comp.specification.z
From: jon@cs.washington.edu (Jon Jacky)
Subject: Trees in Z (was: common data structures in Z)
Summary: Model a tree as a relation, not as records with embedded pointers
Keywords: Z, tree, formal specification
Organization: Computer Science & Engineering, U. of Washington, Seattle
Date: Mon, 25 Jan 93 19:50:22 GMT

C. M. Sperberg-McQueen <U35395@uicvm.uic.edu> writes:

> I'm having trouble formulating a good definition of trees,
> despite the example of a definition of a binary tree in Spivey's manual. ...
>
> (complicated attempt using free types omitted...)
>
> I seem to be headed toward a bewildering tangle ...
>
> It's hard to believe that Z has been in use for over ten years without
> anyone needing to specify arbitrary trees!  How did you do it?

This generic schema summarizes some techniques I've seen.  You don't need to
bother with free types, and you don't need recursive data structures.  Remember
that any graph composed of nodes and arcs can be modelled by a relation.  A
tree is just a special case:

	+--Tree[Node]---------------------------
	|  nodes: P Node
	|  root: Node
	|  parent: Node -+> Node
	|  children: Node <-> Node
	+---------------------------
	|  root e nodes
	|  dom parent U ran parent = nodes	
	|  dom parent = nodes \ {root}
	|  children = parent~
	|  parent+ \cap id = empty
	+--------------------------------------

Parent is declared to be a function, not a relation, to say that a node can
have only one parent.

In order, the predicates say:

- The root is a node.
- All the nodes are connected, and everything that is connected is in nodes.
- Every node except the root has a parent.
- The children relation is just the inverse of the parent function.
- There aren't any cycles - no node is its own ancestor.   This is expressed
  by saying the transitive closure of parent doesn't intersect the identity
  function.  

I think that does it.

The key idea here is that structure of the tree is given by the parent function
(or, equivalently, the children relation).   You do not need to include any
embedded "pointers" (or references or names or whatever you want to call them)
in the Node data type itself; there is no need for recursive data definitions.
It's important that Node can be almost any data type, it doesn't need to have
been designed in advance to fit into a tree. 

I think the problem with the attempt in the original posting was that it was
too close to an implementation.  Instead of just modelling the tree itself as a
relation, it tried to model the *implementation* of a tree as a data structure
made out of records with embedded pointers.  

Jonathan Jacky				jon@radonc.washington.edu
Radiation Oncology RC-08		voice:	(206)-548-4117
University of Washington		FAX:	(206)-548-6218	
Seattle, Washington  98195
USA
From: mzs@doc.ic.ac.uk (M Zvi Schreiber)
Newsgroups: comp.specification.z
Subject: Re: J.R. Abrial e-mail address and B references
Date: 22 Jan 1993 09:57:59 GMT
Organization: Dept. of Computing, Imperial College, University of London, UK.
Distribution: comp
NNTP-Posting-Host: wombat.doc.ic.ac.uk

I don't have an e-mail, but Jean-Raymond Abrial is at:

26 rue de Plentes
Paris 14

Tel +33 1 45 42 83 49

Hope this helps.

Zvi Schreiber
Data Connection Limited
From: kirby@xerox.com (Mike Kirby)
Newsgroups: comp.specification.z
Subject: Z and other design methodologies
Date: 26 Jan 93 15:46:10 GMT
Article-I.D.: spectrum.1993Jan26.154610.27454
Reply-To: kirby@xerox.com
Organization: Xerox Corporation, Webster NY

I am a new user to Z.  I've picked up most of the syntax.  But I have some questions
about how to go about applying it.  One of the most useful features of your 
traditional design and analysis methodologies (like rumbaugh, shlaer/mellor, etc..) is
the state-transition diagram.  Is there a way in Z to model not only the
states, but the transitions into and outof different states?  It would be
nice if I could specify states, and then when  I specify my member functions
I can describe the state that this function is valid for. 

I am using the Object-Z Specification descripted in TR91-1 from Duke et al.
Is there a newer specification that is available?  

Thanks,
Mike Kirby
Xerox Corp
E-mail: kirby.roch803@xerox.com

Refs:

Roger King, et al., "The Object-Z Specification Language, Version 1,"  Technical
Report 91-1, University of Queensland, Queensland Australia, May 1991
From: mike@comlab.ox.ac.uk (Mike Spivey)
Newsgroups: comp.specification.z
Subject: Re: Trees in Z (was: common data structures in Z
Date: 27 Jan 93 18:28:33 GMT
	<1993Jan26.002530.20610@zia.aoc.nrao.edu>
Organization: Oxford University Computing Laboratory, UK
Originator: mike@client6.comlab
In-reply-to: cflatter@nrao.edu's message of 26 Jan 93 00:25:30 GMT


There's been some discussion about describing a generic model of trees
in Z.

Generic free type definitions are not in the language described in the
Z Reference Manual because I wasn't able to work out how to give them
a meaning in the kind of set theory I was using.  The crucial
difference between Z and functional programming languages like ML is
that constructions in Z are described with all the power of
first-order logic, so are not continuous, as the constructions
definable in ML are.  Non-generic type definitions are handled by
showing how to translate them into a given set declaration and an
axiomatic description, but this translation doesn't work for generics.

In the case of sequences, we get around the problem that there are no
generic free type definitions by constructing an explicit model: a
sequence over X is a function from an initial interval of the natural
numbers to the set X.  (Not quite: historical accident makes Z's
sequences start at 1 instead of 0 as they should -- there's flame
bait!)  This has the added advantage that we can define functions on
sequences "by construction" as well as by recursion.

We can do the same thing for various kinds of homogeneous trees: a
tree over X is a function from paths to X with a domin that is closed
under taking prefixes.  A path is a sequence of some kind of "step";
for example, you get binary trees by taking a step to be either 'L' or 'R'.

So the tree

			1	
			|
		+-------+-------+
		|		|
		2		5
		|
	+-------+-------+	
	|		|
	3		4

would be represented in the model by

	{ <> |-> 1, <L> |-> 2, <L,L> |-> 3, <L,R> |-> 4, <R> |-> 5 }


Different flavours of tree are obtained by taking different notions of
"step", and maybe adding extra closure conditions.  For example, trees
where every node has a sequence of children are obtained by taking
steps to be naturals, with the closure condition that

	s ^ <i> in dom T and j < i ==> s ^ <j> in dom T.

This model lets you define all the usual tree operations, and having
explicit paths lets you deal easily with specifications that have a
tree and a current place in the tree -- like a file system that has a
current directory.

-- Mike Spivey

+-----------------------------+-------------------------------+
| Mike Spivey,                | Phone:  (0865) 273838 (Work)  |
| Programming Research Group, |         (086 736) 641 (Home)  |
| 11, Keble Road,             | FAX:    (0865) 273839         |
| Oxford, OX1 3QD, England.   | E-mail: mike@uk.ac.oxford.prg |
+-----------------------------+-------------------------------+
Newsgroups: comp.specification
From: weimin@sce.carleton.ca (Weimin Ma)
Subject: Specifications in UNITY
Summary: Call for pointers to recent development on UNITY as a specification
Keywords: UNITY, specification
Organization: Carleton University
Date: Sat, 23 Jan 1993 05:16:53 GMT

Can anyone give more pointers on UNITY as a software specification language?
I am aware of the recent discussions on UNITY implementations. Please send
replies directly to 
      weimin@sce.carleton.ca
Thanks.

--
Weimin Ma
From: putlock@protocol.zycad.com (Gary Putlock)
Newsgroups: comp.specification
Subject: Uninterpreted modelling system
Date: 21 Jan 1993 10:02:51 -0500
Organization: Protocol, a Division of ZYCAD Corporation
Distribution: world
Reply-To: dominick@protocol.zycad.com
NNTP-Posting-Host: khan.protocol.zycad.com
Keywords: Simulation, uninterpreted, modelling


I am seeking information on the University of Virginia's uninterpreted modelling system.  Any references, papers, etc. will be appreciated. 

Thanks in advance,

Gary Putlock
putlock@protocol.zycad.com

Protocol, A Division of Zycad Corp.
500 International Dr.
Mt. Olive, NJ 07828-1381


Newsgroups: comp.specification,comp.specification.z
From: cianca@cs.unibo.it (Paolo Ciancarini)
Subject: Z and Larch
Organization: Laboratory for Computer Science, University of Bologna, Italy
Date: Tue, 26 Jan 1993 15:46:10 GMT

This year I am teaching a class on software engineering.
I choose to focus on specification;
I (ill) defined a project, and my student are working
on formalizing it in Z. Then they will use Larch
for the design phase.

I would like to know if there are any other courses
that are using the same combination: Z for
requirement analysis and specification document,
and Larch for specification analysis and design document.

I am aware of the paper by prof. Garland in the last
Sw Eng Education Conference (published in Springer LNCS).

I would like to exchange ideas and problems...

Paolo Ciancarini
Univ. of Bologna
-- 
Paolo Ciancarini
Dept. of Mathematics 
Univ. of Bologna -  Pza di Porta S.Donato 5, 40126 Bologna Italy
tel +39 51 354496
Newsgroups: comp.specification
From: tim@catt.citri.edu.au (Tim Liddelow)
Subject: SDL CASE tools available ?
Keywords: SDL, CASE
Reply-To: tim@catt.citri.edu.au
Organization: CATT Centre at CITRI
Date: Sun, 24 Jan 93 06:02:13 GMT

Could anyone let me know of any tools that are available for SDL/GR entry and SDL/PR
production ?  I am also interested in the prices of these tools.

Thanks in advance

Tim.


---
________________________________________________________________________________
  Tim Liddelow                                          for(;;) fork();
  Systems Programmer
  Centre of Advanced Technology in Telecommunications   My brain on a bad day.
  CITRI, Melbourne, Australia                           
  internet : tim@kimba.catt.citri.edu.au                
  Phone : +61 3 282 2455   Fax : +61 3 282 2444	        
________________________________________________________________________________

Newsgroups: comp.specification
From: pgl@imada.ou.dk (Peter Gorm Larsen)
Subject: FME'93 Call For Posters
Keywords: formal methods, vdm, z, raise, lotos, estelle, specifications
Organization: Dept. of Math. & Computer Science, Odense University, Denmark
Date: Thu, 21 Jan 1993 14:38:01 GMT

Formal Methods Europe '93 --- Call For Posters

We have decided to have a poster session at the FME'93 Symposium.
Thus, if you are planning to attend FME'93 please let me know if
you are interested in having some posters displayed.
Please indicate how many units of A3 size you would like
and explain what will be on the posters. It will be free to display
posters, but unfortunately it will not be possible to give presentations
about their contents. On the other hand there will be a notice board 
where attendees which are interested in a particular poster can inform
about his interest such that a face-to-face discussion can be obtained.

The posters can contain anything related to formal methods. Thus,
tools currently under development, teaching material, new books
or journals, projects which have used or are using formal methods,
even advertisments for formal methods courses are acceptable.
The posters are welcome to be supported by copies of a report or
similar. The posters do not need to be sent here, but can be handed
over at the registration desk at arrival. So far we have reservations
for the first 12 A3 size units.

Peter Gorm Larsen
Organizing chairman FME'93
The Institute of Applied Computer Science (IFAD)
Forskerparken 10, DK-5230 Odense M, Denmark
Phone: +45-65932300, Fax: +45-65932999, Email: peter@ifad.dk
From: augustss@cs.chalmers.se (Lennart Augustsson)
Newsgroups: comp.specification
Subject: Summer School: TYPES FOR PROOFS AND PROGRAMS
Date: 21 Jan 93 15:53:46 GMT
Reply-To: baastad@cs.chalmers.se
Organization: Dept. of CS, Chalmers, Sweden


			 INTERNATIONAL SUMMER SCHOOL

				      ON

			TYPES FOR PROOFS AND PROGRAMS

		      BAASTAD, SWEDEN, JUNE 7 - 18, 1993


During the last few years major achievements have been made in using
computers for interactive proof developments. Several proof assistants
(such as Coq, Lego, and Alf) have been developed based on the idea of
a logical framework in which it is possible to define a variety of
logics. Many quite substantial proofs from mathematics, logic, and
computing have also been implemented in them.

This two week course is for postgraduate students and researchers who
want to learn about interactive proof development. There will be
introductory and advanced lectures on lambda calculus, type theory,
logical frameworks, program extraction, and other topics which give
relevant background.  No prior knowledge of these topics is expected.

The systems will be demonstrated, and students will get extensive
opportunities to use them in a workstation environment for developing
their own proofs.

List of speakers
----------------
The main speakers are

	Henk Barendregt		Jean-Louis Krivine
	Stefano Berardi		Per Martin-Lof
	Rod Burstall		Michel Parigot
	Thierry Coquand 	Christine Paulin
	Gerard Huet		Randy Pollack

Location
-------- 
The summer school will be held in Baastad, a small town between
Copenhagen and Gothenburg on the Swedish west coast.

Scholarships
------------
There is a limited number of scholarships available for people who
cannot obtain funding for their travel, participation fee and living
expenses.  A request for full or partial support should be enclosed
with the application.

Fees
----
The participation fee is 4 000 SEK and room and board is 4 000 SEK.

Applications
------------
Applications with a C.V. and a letter of recommendation should be sent to

        Bengt Nordstrom
        - summer school -
        Department of Computer Sciences
        Chalmers Technical University
        S - 412 96 Gothenburg, Sweden
        e-mail: baastad@cs.chalmers.se

The DEADLINE for application is April 15, 1993.

Organization
------------

The school is organized by the ESPRIT Basic Research Action `Types for
Proofs and Programs'. The local organization is done by Bengt
Nordstrom, Peter Dybjer, Jan Smith, and Bjorn von Sydow, Gothenburg.


-- 

	-- Lennart Augustsson
[This signature is intentionally left blank.]
From: karlis@cs.chalmers.se (Karlis Cerans)
Newsgroups: comp.specification
Subject: CCITT documents wanted
Date: 23 Jan 93 13:32:17 GMT
Distribution: comp.specification
Organization: Dept. of CS, Chalmers, Sweden

Does anyone know where to get access to the latest (1992) versions of
the official CCITT descriptions of SDL and MML (Man Machine Language)?

Does anyone know about the existence and coordinates of a MML User's
club on Internet?

A friend of mine is going to write a small telephone exchange and he 
needs these documents.

Any information (to the net or by email appreciated).

Thanks in advance,

Karlis Cerans.

Email: karlis@cs.chalmers.se
Newsgroups: comp.parallel
From: srikant@skorpio.usask.ca (Srikant Subramaniam)
Subject: Loop Scheduling with dependencies
Organization: University of Saskatchewan, Saskatoon, Canada
Date: 25 Jan 1993 01:12:36 GMT

Hello Netters:

I would appreciate receiving some info on the topic of scheduling of loops
with dependencies. 

Thanks ahead ...

-- 
Srikant Subramaniam.
srikant@cs.usask.ca 

Newsgroups: comp.parallel
From: apofort!metcalf@dxmint.cern.ch (Michael Metcalf )
Subject: Re: Wanted: Folk Theormes in Fortran Programming
Apparently-To: comp-parallel
Organization: CERN European Lab for Particle Physics
Date: Wed, 27 Jan 1993 14:41:06 GMT

steve@hubcap.clemson.edu ("Steve" Stevenson) writes:

>I am trying to make a catalog of folk wisdom in fortran programming. I already
>have a some theorems.  For example:
>        BAD           GOOD
>x = y/2.0          x=y*0.5
>a**5               (a*a)*(a*a)*a
>2.0*x              x+x

>I would appreciate any such words of wisdom you might have.


I collected such wisdom some time ago and published
it as "FORTRAN Optimization", Academic Press, 1985,
ISBN 0-12-492482.4.

   Hope this helps,

                  Mike Metcalf


Newsgroups: comp.parallel
From: jdb@arp.anu.edu.au (John D. Barlow)
Subject: finding compute resources (was Re: World's most powerful computing)
Organization: Centre for Information Science Research, ANU, Canberra, Australia
Date: 22 Jan 1993 02:20:08 GMT

In article <1993Jan21.013116.1925@sol.cs.wmich.edu>, john@cs.wmich.edu (John Kapenga) writes:
|> If there is a use for such a list it might be to allow those who
|> have no idea what's going on to find out where various non-conventional
|> computers are located.
|> 
|> Listing a site, brief information on access, uses and a list of hardware
|> (without the vendor hype) might help someone.

Try the internet resource guide.  It does this.  If your office is not
on it, then contact the resource-guide organisers.

To find the Internet resource guide, try archie.  There should be copies
on most big FTP sites (uunet.uu.net  ??).

-- 
John Barlow, Parallel Computing Research Facility, I-Block,
Australian National University, Canberra, 0200, Australia.
email = John.Barlow@anu.edu.au
[International = +61 6, Australia = 06] [Phone = 2492930, Fax = 2490747]

Newsgroups: comp.parallel
From: earl@cerebus.pilot.dmg.ml.com (Earl Chen)
Subject: Novice needs info on parallel libraries
Organization: Merrill Lynch Debt Markets Group
Date: Thu, 28 Jan 1993 17:06:27 GMT


Request for help and advice.

I am currently working on a project implementing a parallel environment
across several Sun Sparc's using c-Linda from SCA.  What other environments,
libraries, etc. are available that would give me capabilities similar to c-Linda.

Thank you for your time,

Earl Chen
E-mail: earlchen@aol.com

Newsgroups: comp.parallel