HDTenEightyP/NetNews huggingface dataset:
From: cash@auric.uni-koblenz.de (Martin Carstensen)
Newsgroups: comp.specification.z
Subject: Re: About Genericity...
Date: 27 Jul 92 10:02:45 GMT
Reply-To: cash@informatik.uni-koblenz.de
X-Mailer: ELM [version 2.3 PL11]
X-Mailer: mail-news 2.0.3

Donatella Castelli writes: 
| 
| In ZRM, a generic constant definition is restricted to having a value
| uniquely determined for each possible formal parameter.
| Now, I think it is sometimes useful to be able to define a generic
| object, without having to state this uniqueness condition.

The reason for this requirement is given in ZRM too (the example of the
erroneous left/right definition). 
Nevertheless: Sometimes I share your wish ;-)

| For example, I would like to define basic properties of any partial order
| among values of an as-yet-unknown type X with a generic variable
| definition
| 
|          ===[X]==========================
|          |
|          |    G  :   X <-> X
|          |
|          |----------------------
|          |
|          |    -- reflexivity --
|          |    -- antisymmetry --
|          |    -- transitivity --
|          |___________________________
| 

In this case you should define the set of all orders themselves as 
generic constants, e.g. as pre-generics:

===[X]===========================
|
|  porder _ , torder _ : P (X <-> X)
|
|---------------
|
|        -- some predicates for reflexivity and such --
|
|________________________________


For relations of whatever type you can require of them to be orders:

|  o1 : N <-> N
|  o2 : P N <-> P N
|----------------
|  torder o1
|  porder o2


| For example, if N is the set of natural numbers, I would like to
| constrain the instance G[N]  to be the usual order _<=_ , writing
| 
|       G[N]  =  (_<=_)

For particular orders of any type you have to give different, arbitrarily
chosen definitions like    o1 = (_ <= _)    and     o2 = "subset_on_N".
But how can you compare such different orders?


Regards,
	Martin

-- 
+------------------------------------------------------------------------
| Martin Carstensen, Koblenz University         cash@infko.uni-koblenz.de
|        Department of Computer Science         Voice: +49 261 9119-423
|        Rheinau 3-4, D-5400 Koblenz, Germany   Fax:   +49 261 9119-499
Newsgroups: comp.specification.z
From: Donatella Castelli <castelli@iei.pi.cnr.it>
Subject: About Genericity...
Organization: IEI-CNR
X-Useragent: Nuntius v1.1
Date: Fri, 24 Jul 1992 12:48:20 GMT
X-Posted-From: mac-castelli.iei.pi.cnr.it
X-Posted-Through: sol.ctr.columbia.edu


In ZRM, a generic constant definition is restricted to having a value
uniquely determined for each possible formal parameter.
Now, I think it is sometimes useful to be able to define a generic
object, without having to state this uniqueness condition.
We could call this object a "generic variable" and any standard generic
constant could be considered a particular instance of a generic variable.

For example, I would like to define basic properties of any partial order
among values of an as-yet-unknown type X with a generic variable
definition

         ===[X]==========================
         |
         |    G  :   X <-> X
         |
         |----------------------
         |
         |    -- reflexivity --
         |    -- antisymmetry --
         |    -- transitivity --
         |___________________________


After defining a generic variable G, we would need to be allowed to add
further constraints about it, by means of a predicate used as a
paragraph, as though G were a common global variable.

For example, I would like to constrain the previously defined generic
variable G to be  total.

  But above all, we would need to be allowed to add constraints about
"any instance" of G, without affecting any other instance of G.

For example, if N is the set of natural numbers, I would like to
constrain the instance G[N]  to be the usual order _<=_ , writing

      G[N]  =  (_<=_)


I am very interested in your opinion about the feasibility of the
extension to Z, and in your knowledge of any literature about it.

Thank you in advance.

address: Donatella Castelli
  IEI - CNR
  via  S. Maria 46, Pisa
  Italy

e_mail:  castelli@iei.pi.cnr.it
From: ana@GCTC.ITEP.BR
Newsgroups: comp.specification.z
Subject: RE: Object Z references
Date: 23 Jul 92 23:30:00 GMT
X-Envelope-To: zforum@comlab.ox.ac.uk
X-Mailer: mail-news 2.0.3


 
The ZIP report "Comparative Study of Object Orientation in Z" presents MooZ
(Modular Object Oriented Z), a Z extension aimed at large software systems
specifications. It was originally proposed in
 
@inproceedings{MC90,
   author = {S. R. L. Meira and A. L. C. Cavalcanti},
   address = {Oxford - UK},
   booktitle = {Workshop on Computing Series},
   editor = {Prof.\  C. J. van Rijsbergen},
   month = dec,
   pages = {173 -- 192},
   publisher = {Springer-Verlag},
   title = {{Modular Object-Oriented Z Specifications}},
   year = {1990}
}
 
The latest reference is
 
@techreport{MC92b,
   author = {S. R. L. Meira and A. L. C. Cavalcanti},
   address = {Recife - PE},
   institution = {Universidade Federal de Pernambuco,
                  Departamento de Inform\'atica},
   title = {{The MooZ Specification Language}},
   year = {1992}
}
 
which can be get via ftp from
 
machine: gctc.itep.br (150.161.1.2)
user: anonymous
directory: pub/MooZ
file: MooZ.ps.Z
 
or by e-mailing me a request.
 
Ana Lucia Cavalcanti
From: tcskcl@aie.lreg.co.uk ("K." Lano)
Newsgroups: comp.specification.z
Subject: Re: Object Z references
Date: 21 Jul 92 09:21:17 GMT
X-Mailer: mail-news 2.0.3



Yet another object-oriented Z is Z++, as summarised in a paper in 
the proceedings of ECOOP 92: ``Reasoning and Refinement in Object-Oriented 
Specification Languages", and given in detail in a report ``The Z++ Manual"
available from Dr H. Haughton, Lloyds Register of Shipping, 29 
Wellesly Rd., Croydon CRO 2AJ.
From: amg@ecs.soton.ac.uk (Andy Gravell)
Newsgroups: comp.specification.z
Subject: Re: About Genericity...
Date: 27 Jul 92 09:07:34 GMT

In <1992Jul24.124820.28528@ctr.columbia.edu> castelli@iei.pi.cnr.it (Donatella Castelli) writes:


>In ZRM, a generic constant definition is restricted to having a value
>uniquely determined for each possible formal parameter.
>Now, I think it is sometimes useful to be able to define a generic
>object, without having to state this uniqueness condition.
>We could call this object a "generic variable" and any standard generic
>constant could be considered a particular instance of a generic variable.

>For example, I would like to define basic properties of any partial order
>among values of an as-yet-unknown type X with a generic variable
>definition

  ... 39 lines deleted ...

What about defining as a generic constant the set of *all* partial
orders on X?  Then you can introduce as a constant some particular
partial order drawn from this set.  eg to introduce a new partial
ordering on the naturals you can write

  G: PartialOrder[Nat]

You can then further constrain G as you wish, perhaps by

  G = (_ <= _)

Would this construct do for your "generic variable"?

Andy Gravell
From: cash@auric.uni-koblenz.de (Martin Carstensen)
Newsgroups: comp.specification.z
Subject: concrete syntax and fuzz
Date: 23 Jul 92 17:26:45 GMT
Reply-To: cash@informatik.uni-koblenz.de
X-Mailer: ELM [version 2.3 PL11]
X-Mailer: mail-news 2.0.3

The concrete syntax of fuzz differs slightly from the one LaTeX produces
from specifications (e.g. fuzz syntax contains the string "\forall"
where LaTeX produces the quantor symbol itself, schemas are more
complicated examples).

These differences can be utilized to some extent. If you want the
(unparenthesized) argument to a function written as subscript you can
get this by defining:

	\newcommand{\f}[1]{f_{#1}}
	\begin{gendef}[INDEX]
	\f : INDEX \fun \nat \pfun \nat
	\end{gendef}

Recently I tried to define strings like this:

	\begin{zed}
	LETTER ::= a|b|c|d \\
	STRING ::= string \ldata \seq LETTER \rdata
	\end{zed}
	
Now I'm looking for a way to tell LaTeX what strings shall look like
and which will be accepted by fuzz. The following approach would be
treated properly by fuzz, but the LaTeX definition does only do half 
of the job.

	\newcommand{\str}[1]{"#1"}
	%%\begin{zed}
	%%\str == string
	%%\end{zed}

	\begin{axdef}
	s: STRING
	\where
	s = string \langle a, b \rangle \\
	s = \str {\langle a, b \rangle}
	\end{axdef}

Any idea?

-- 
+------------------------------------------------------------------------
| Martin Carstensen, Koblenz University         cash@infko.uni-koblenz.de
|        Department of Computer Science         Voice: +49 261 9119-423
|        Rheinau 3-4, D-5400 Koblenz, Germany   Fax:   +49 261 9119-499
From: brendan@cs.uq.oz.au (Brendan Mahony)
Newsgroups: comp.specification.z
Subject: Re: concrete syntax and fuzz
Date: 24 Jul 92 01:44:53 GMT
Reply-To: brendan@cs.uq.oz.au

In <9207231534.AA00732@auric> cash@auric.uni-koblenz.de (Martin Carstensen) writes:

| The concrete syntax of fuzz differs slightly from the one LaTeX produces
| from specifications (e.g. fuzz syntax contains the string "\forall"
| where LaTeX produces the quantor symbol itself, schemas are more
| complicated examples).

| Recently I tried to define strings like this:

| 	\begin{zed}
| 	LETTER ::= a|b|c|d \\
| 	STRING ::= string \ldata \seq LETTER \rdata
| 	\end{zed}
| 	
| Now I'm looking for a way to tell LaTeX what strings shall look like
| and which will be accepted by fuzz. The following approach would be
| treated properly by fuzz, but the LaTeX definition does only do half 
| of the job.

| 	\newcommand{\str}[1]{"#1"}
| 	%%\begin{zed}
| 	%%\str == string
| 	%%\end{zed}

| 	\begin{axdef}
| 	s: STRING
| 	\where
| 	s = string \langle a, b \rangle \\
| 	s = \str {\langle a, b \rangle}
| 	\end{axdef}

I am not sure your solution works at all for the new version of fuzz, at
least we have had troubles with spurious {..} pairs.

Anyway, you need to appeal to a little TeX (i.e. use \def rather than
\newcommand). In general if you want to produce a novel concrete syntax
for a function application use a TeX definition like

\def\f(#1){...}

Now you can write \f(arg) in your Z, get fuzz to accept it, and get
LaTeX to print it any old how. (This idea was suggested by Mike Spivey)

I your case you need to redefine the TeX output of \langle .. \rangle.
Try this:

\def\str(#1){\def\langle{\mathopen{\mbox{``}}}\def\langle{\mathopen{\mbox{``}}}#1}

You list now appears within quotes rather than < .. > brackets.

I am not as clear on how to get rid of the commas. Some trick with a
\mathchardef or \mathcode I suppose. I don't think you can trick fuzz
into accepting some character other than the comma. Find a copy of the
TeXbook.
--
When soldiers form lines or hollow squares, you call it reason.
When wild geese in flight take the form of a letter V, you say instinct.
When the homogeneous atoms of a mineral arrange themselves into shapes
mathematically perfect you have nothing to say. You have not even invented a name to conceal your heroic unreason."
Newsgroups: comp.specification
From: naren@cs.UAlberta.CA (Narendra Ravi)
Subject: Re: Looking for specs of phone system
Organization: University of Alberta, Edmonton, Canada
Date: Mon, 27 Jul 1992 17:36:22 GMT

anthony@cs.uq.oz.au (Anthony Lee) writes:

: In <1992Jul24.025140.11391@siswat.hou.tx.us> buck@siswat.hou.tx.us (Lester Buck) writes:

: >In article <dk.711659792@alcor> dk@alcor.concordia.ca (dimitri k) writes:
: >>I'm looking for specifications (preferably formal) of a phone 
: >>system---a plain old telephone system (POTS) will do.  The spec
: >>lang or method isn't a concern.  Ftpable sources welcome...
: >>
: >>dk


: >I got a report from the University of Queensland in Australia which
: >is a Z specification of Switching System 7 (if I remember).  It
: >covers the user, network, and switching center levels as the
: >detail increases.

: I have written a specification of the basic telephone network in
: Object-Z.  Send me your snail mail address and I will send you
: the tech report.
: --
: Anthony Lee (Time Lord Doctor) (These are my opinions !)
: email: anthony@cs.uq.oz.au	voice:+(61)-7-3651204 FAX:+(61)-7-3651999
: SNAIL: Department Computer Science, The University of Qld, 
:        St Lucia, Qld 4072, Australia

There is one in the book _Software Engineering Mathematics_. One of the
authors is J. Woodcock.

-- 

 -- Naren
    Narendra Ra[a]vi     Email : naren@cs.ualberta.ca
--

 -- Naren
    Narendra Ra[a]vi     Email : naren@cs.ualberta.ca
Newsgroups: comp.specification
From: haim@dancer.uucp (24103-kilov)
Subject: CFP: OOPSLA Workshop on serious oo reasoning in information modeling
Organization: Bellcore, Livingston, NJ
Date: Thu, 23 Jul 92 22:11:22 GMT


Serious object-oriented reasoning in information modeling



The conscious use of abstraction is very well understood in the programming
world. Investigation is needed for better use of abstraction in information
modeling. One of the major issues here is how to describe information (data +
behavior) independently of how it is stored or used. Among the questions to be
addressed:

How do you represent a "conceptual schema" using an object approach? In
particular, how do you represent a relationship? How do you specify object
operations? How do you represent operations spanned across several objects?

Does the "entity-relationship approach" to information modeling lack behavior?

How can you specify behavior in an implementation-independent manner?

What is the "impedance mismatch" problem for the object paradigm?

Is API specification consistent with the object approach?

Is it possible to create an Object SQL and not delete anything from SQL?

Is it possible to do object programming in <your favorite programming language>?

How can you represent catalogs of data elements and encyclopedic resources for
information management with regard to representation of behavior?

Position papers are not to exceed three pages and are due no later than August
15, 1992. Submissions by e-mail are strongly encouraged. Participants will be
selected based on the interest and quality of their position papers. Suggestions
for possible panels and their participants are also welcome. Some accepted
position papers will be chosen for presentation at the workshop. Applicants will
be notified of acceptance by September 15 and will receive a copy of the
position papers.

Workshop organizers: 

Bill Harvey, Robert Morris College, Coraopolis, PA, 
and 
Haim Kilov, Bell Communications Research, Morristown, NJ


Contact information:
Haim Kilov, Bell Communications Research, MRE 1F216, 435 South Street,
Morristown, NJ 07960
(Phone: 201-829-2816; Fax: 201-829-5678, e-mail: haim@bcr.cc.bellcore.com
or
haim@dancer.cc.bellcore.com)

(The date of the Workshop is Sunday, October 18, 1992).
From: pkdf@dcs.ed.ac.uk (Peter Froome)
Newsgroups: comp.specification
Subject: SpecBox: a formal methods tool for VDM
Date: 22 Jul 92 08:15:54 GMT
Reply-To: pkdf@dcs.ed.ac.uk (Peter Froome)
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U

SPECBOX VERSION 2.21
____________________

A new version of Adelard's formal specification support tool for 
draft BSI/ISO VDM has now been released.  The new version has several 
improvements and enhancements over older versions, including the 
following:

*	A revised grammar, reflecting the latest draft standard
*	An improved LaTeX facility
*	An improved, much faster, semantic analyser
*	An interface to the Mural proof assistant

Prices now run from 495 to 1995 UK pounds for single user supported 
licences, with academic site licences between 250 and 500 UK pounds.


DESCRIPTION

SpecBox is an industrialised tool for inputting, checking and 
printing VDM specifications.  It is composed of four main parts:

*	A syntax checker
*	A LaTeX generator
*	A semantic analyser
*	A Mural translator

The syntax checker is used to input specifications in the ASCII form 
of BSI/ISO VDM and check them for grammatical errors.  The checker 
comprises an editor linked to a parser; it gives help on the valid 
VDM terms to enter at each stage, and also enables the grammar to be 
investigated and particular syntactic classes to be chosen.  It also 
completes phrases (by closing brackets, for example) automatically.

The LaTeX generator produces a source file for the LaTeX document 
preparation system that will print the specification in the 
mathematical syntax.  Line numbering, cross-references and subscripts 
are supported.

The semantic analyser carries out checks on the well-formedness of 
the specification.  These checks include matters such as declaration, 
scope, number of arguments, use of state variables and hooked values, 
use of record types and constructor functions, and use of 'is-
expressions'.  The semantic analyser displays diagnostic messages 
while it is running, and on completion produces a report file, an 
annotated listing and a cross-reference table.  The algorithm used 
for analysis prevents many redundant cascade error messages from 
being generated after the first occurrence of a semantic problem.

The Mural interface enables specifications produced using SpecBox to 
be transmitted to the Mural proof assistant for the generation and 
discharge of proof obligations.  (Mural was developed by Manchester 
University and the Rutherford Appleton Laboratory.)

SpecBox is continually being enhanced: future developments include

*	A version for Microsoft Windows 3.1
*	Mathematical syntax support
*	Full support for BSI/ISO VDM modules

Existing customers receive upgrades at preferential prices.


For further information contact:

Peter Froome
Adelard
Coborn House
3 Coborn Road
London E3 2DA
UK
Tel: +44 (0)81 983 0214
Fax: +44 (0)81 983 1845
Email: pkdf@dcs.ed.ac.uk
Newsgroups: comp.specification
From: zhangj@cognos.com (J. Zhang)
Subject: Re: Looking for SAA - Spec.
Organization: Cognos Incorporated, Ottawa CANADA
X-Newsreader: Tin 1.1 PL3
Distribution: fb20
Date: Thu, 23 Jul 1992 15:48:47 GMT

xmic@opal.cs.tu-berlin.de (Michael Behnke) writes:
: Hi,
: 
: I am looking for some article about SAA (what means SAA exactly?). 
: Is it a graphical user standard created by IBM ?
: What are the guidelines for SAA - programming ?
: 
: Please, if You have some info, post it to this group.
: 
: Michael Behnke.
: 
SAA stands for System Application Architecture, which is a collection of
software interfaces, protocols and conventions that provide the guidlines and
the framework for the development and execution of consistent application. 
Yes, SAA is created by IBM. The Graphical User Standard is just one of the four
element of SAA.  SAA contains:
 
	CUA - Common User Access - the graphical user standard. Microsoft ships it
		  with its Windows 3.x SDK.

	CPI - Common Programming Interface.

	CCS - Common Communications Support.

	Common Application. 

Currently there are about 16 publications in SAA library.

Hope above info helps.
-- 
--------------------------------------------------------------------------------
Jianguo Zhang	Cognos Inc.         Voice Mail: (613)737-6554 (h)
                3755 Riverside Dr.              (613)738-1440 x 3493 (w)
                Ottawa, Ontario     UUCP:     cognos!zhangj
Newsgroups: comp.specification
From: cheeyong@kolmogoroff.iss.nus.sg (Lim Chee Yong)
Subject: SPIN tool enquiry
Originator: cheeyong@kolmogoroff
Organization: Institute of Systems Science, NUS, Singapore
Date: Tue, 21 Jul 1992 05:54:16 GMT

I am looking for more information about the SPIN tool. Anybody
who knows about this tool, and where I can ftp the source, please 
send the info to me by e-mail.

Thanks in advance for any info.


Chee-Yong Lim,

cheeyong@iss.nus.sg
-- 
Lim Chee Yong				 Phone    : 65 - 772 - 3695
Institute of Systems Science  		 Fax      : 65 - 778 - 2571 
National University of Singapore         Internet : cheeyong@iss.nus.sg
Kent Ridge, Singapore 0511               Bitnet   : isslcy@nusvm.bitnet
From: charlot@lri.lri.fr (Francois Charlot)
Newsgroups: comp.specification
Subject: Abstraction and Specification
Date: 27 Jul 92 15:47:38 GMT
Organization: Laboratoire de Recherche en Informatique



Hello users !

I've just started a PhD Thesis in Computer Science, in cooperation
with a French company. The subject of the Thesis is dealing with
specification and I have to use abstraction techniques to specify
a huge software. The fact is that, today, the company didn't write
informal specifications, but they intend to do it (together with me).
The first task I would like to realize is to explain to some folks
of the company what are the interests of abstraction and specification.

The point of my article is to ask ALL of you this question :

Does anybody there know if I could find some experiences in this kind
of work, and do I have any chance to find a simple (but comprehensive and
sufficiently detailed) example of such kind of specification ?

I would be very pleased if I could find the following sources :

          - Informal specification of a "school-problem" (lifts, coffee-
            machine, ...)
          - Abstract formal specification derived from the previous one
          - Refinement of the previous specification (pascal-like for instance)

Everybody around me say that doesn't exist ! 

Actually, I've the "feeling" of what I have to do, but it is definitively not
enough to start my thesis (and my bosses don't care of my "feelings" !).

Please, e-mail me ALL the (even small) informations you know about this
kind of work. It will help me A LOT, because I'm stucked !

(This is the first time I write something in the news ; then, be tolerant !)



			Thanks in advance.



************************************************************************
*********
* Francois CHARLOT                             uunet  :
charlot@lri.lri.fr     *
* L.R.I. - Bat 490 - Universite Paris-Sud      bitnet :
charlot@FRLRI61.BITNET *
* F - 91405 ORSAY CEDEX                        Tel    : (33 (1)) 69 41
70 82   *
************************************************************************
*********
From: janowsky@math.rutgers.edu (Steven Janowsky)
Newsgroups: comp.parallel
Subject: Re: Could I compete the low-end CM5 with multiple SPARCstations?
Date: 24 Jul 92 18:19:47 GMT
Organization: Rutgers Univ., New Brunswick, N.J.


In article <1992Jul23.154028.11687@unocal.com> stgprao@xing.unocal.com (Richard Ottolini) writes:

> (1) Each node of CM-5 contains a 128 megaflop array processor (actually four
> 32 MF vector chips if you buy the full configuration.)  This an order of
> magnitude faster than the fastest SPARC chip.

Current CM5 configurations DO NOT have these vector chips.  Or at least
none of the CM5's that I have access to have them yet.
Until they arrive...

> (2) The communication channels between the nodes scales with the number of
> processors on a CM-5 in contrast to a workstation network that subdivides
> traffic on a single network.  We do distributed number crunching at our
> site on a workstation network.  Network saturation often occurs when the
> number of nodes are in the low double digits.

32 = low double digits.  For certain low-communication applications, the
network of SS's should be better.  For my applications, where I want to
get STATISTICS, I'd be better running 32 independent copies of the
program on each machine and then have ZERO communication.

> (3) SOFTWARE, SOFTWARE, SOFTWARE!  to paraphrase a real estate maxim.
> TM is attempting to implement their data-parallel programming languages-
> TM-FORTRAN-90/HPF and others- that hide need to worry a lot about how to
> distribute data and communications.

How much overhead do you think the compiler eats up ?  I.e. do you
really get 32 procs of power?   On the CM2/200 I am playing compiler
games in order to approach theoretical max speed.  Those more dedicated
than me make PARIS calls directly.

SJ
Newsgroups: comp.parallel