HDTenEightyP/NetNews huggingface dataset:
From: houkes@ebq.eb.ele.tue.nl (Vincent Houkes)
Newsgroups: comp.music
Subject: signature for question about notation-program for IBM-PC (MSDOS)
Date: 2 Oct 92 10:25:25 GMT
Distribution: eunet
Organization: Eindhoven University of Technology, The Netherlands


 
 I have asked a question about notation-programs but alas my
signature was not merged into the question. So here is my signature.
 Sorry that it happened.




V.J. Houkes                                      \    /   /
 Student University of Technology of Eindhoven     \  /---/
 E-Mail :  houkes@eb.ele.tue.nl                     \/   /
Newsgroups: comp.music
From: "Christoph Luebbe" <UJ4J@DKAUNI2.BITNET>
Subject: SCORE user needs help
Organization: University of Karlsruhe, Germany
Date: Mon, 28 Sep 1992 20:02:38 GMT

Hi
..
I am a Score user (V3.08) and a am very shure to have the best
musical score layout programm on the market.
But now I have a little problem. I changed from MS-Dos 5 to
OS/2. This is really great because you can run SCORE,the PAGE
layout program, and a postscript emulator at the same time, but
there is a problem with my MUSIC QUEST PC Midi Card (it is
compatible to Roland MPU401). SCORE can send MIDI data but it is
not able to receive any MIDI data. I tried all possible interrupts
but i was not able to solve the problem. Remember all works fine
under DOS. Any ideas ?
..
please contact me. Christoph Luebbe uj4j@dkauni2.bitnet    or
                   uj4j@ibm3090.rz.uni-karlsruhe.dbp.de
From: leongaw@hpcc01.corp.hp.com (Ak Wing Leong)
Date: Wed, 30 Sep 1992 08:52:25 GMT
Subject: MacGyver's theme song
Organization: the HP Corporate notes server
Newsgroups: comp.music

Sometime ago I came across a request for MacGyver's theme song. I posted
a request for a copy but till now had not received it yet ? Any kind soul
out there who has one please email me ?
Newsgroups: comp.music
From: hsiaoe@aix.rpi.edu (Eric Hsiao)
Subject: MOD player for Sun IPX?
Organization: Rensselaer Polytechnic Institute, Troy, NY
Date: Sun, 4 Oct 1992 20:21:40 GMT

Does there exist a .MOD player for a Sun Sparc IPX color machine?
If so, where can I get the binary (or source code)?
             - Eric
-- 
| Internet: hsiaoe@rpi.edu         > Read GIF News - a freely copied news  < |
| Bitnet: userHA6G@rpitsmts.bitnet > magazine in .GIF file format.  Color  < |
| To get GIF News, FTP to here:    > articles on reviews of programs,      < |
| netserv1.its.rpi.edu /pub/misc   > games, industry news, IBM, Amiga, etc.< |
Newsgroups: comp.music
From: johnd@lloyd.Camex.COM (John Duesenberry)
Subject: High-Level Granular Synthesis: Code Examples?
Organization: Camex Inc., Boston MA
Date: Fri, 02 Oct 1992 10:38:44 EDT

Does anybody know a source of code examples (preferably in CSound or C)
that implement granular synthesis at a higher level? That is, not
instruments that synthesize individual grains (which is quite simple)
but code that will generate events consisting of many grains, with
parametric control - as described by Curtis Roads in several of his
articles. I am limited to CSound on a Mac, so something that works
in that environment would be preferable. 
Any help or pointers would be appreciated...
John Duesenberry
From: nether@wpi.WPI.EDU (Joel C Belog)
Newsgroups: comp.music
Subject: Nutation ...
Date: 30 Sep 1992 17:37:52 GMT
Organization: Worcester Polytechnic Institute
Distribution: inet
NNTP-Posting-Host: wpi.wpi.edu


Hi ...

	I'm looking for the Nutation software for the NeXT
	systems.  I looked on ccrma-ftp.stanford.edu but I
	couldn't find it there.  Does anyone know where it 
	is?  On the same thread, does anyone know where I
	can get the Sonata font (for NeXT systems) that 
	Nutation needs?  I called NeXTconnection, but they
	haven't had it in for a long time and their arrival
	dates for it are screwed up.  I called the other
	place ... I forget the name ... the one mentioned in
	the Nutation Readme, but their price is to expensive.

	Also, does anyone know of similar nutation software for the 
	NeXT?  Unix Source?  X11R? source?  Is there an updated FAQ?  
	I just looked at the one posted here a few days ago and 
	it seems dated.  Anyone have an updated version?
 

	Thanks a million ... or two,

	Joel
        ******* <<<<< ((( ALL VALID DISCLAIMERS APPLY ))) >>>>> *******
        ***** <<<<< (((                                 ))) >>>>> *****
        * Joel Belog                   *  e-mail : nether@WPI.wpi.edu *
        * snail mail: 100 Institute Rd *          {NeXTmail Prefered} *
        *             WPI Box 2813     *                              *
        *             Worcester MA     *  voice mail : (508) 791-4840 *
        *                 01609 - 2280 *  flames >> /dev/null         *
        ****** <<<<< (((                               ))) >>>>> ******
-- 
        ******* <<<<< ((( ALL VALID DISCLAIMERS APPLY ))) >>>>> *******
        ***** <<<<< (((                                 ))) >>>>> *****
        * Joel Belog                   *  e-mail : nether@WPI.wpi.edu *
        * snail mail: 100 Institute Rd *          {NeXTmail Prefered} *
Newsgroups: comp.specification
From: rekers@elc2 (Jan Rekers)
Subject: Re: Specifying a ring in LOTOS
Organization: Dept. of Math. and CS, Leiden University, the Netherlands
Date: Fri, 2 Oct 92 09:04:02 GMT

In article <1992Oct1.141058.19700@hasler.ascom.ch> dubuis@tech.ascom.ch writes:
>In article 7536@rulway.LeidenUniv.nl, rekers@elc2 (Jan Rekers) writes:
>> 
>> I wish to define a ring of processes with the following layout:
>> 
>>                      1
>>                     / \
>>                    c   a
>>                   /     \
>>                  3 - b - 2
>
>Here follows my solution:
>
>specification ring : noexit
>behaviour
>  hide b,c in
>    (
>    hide a in
>      ( node1 [c,a]
>        |[a]|
>        node2 [a,b]
>      )
>      |[c,b]|
>      node3 [b,c]
>    )
>where
>  process node1 [p,q] : noexit :=
>     p ; q ; node1 [p,q]
>  endproc
>  process node2 [p,q] : noexit :=
>     p ; q ; node2 [p,q]
>  endproc
>  process node3 [p,q] : noexit :=
>     q ; p ; node3 [p,q]
>  endproc
>endspec

The solution works as it should, but it is somehow asymetrical.

It does a perfect job in hiding the action ``a'', which should be
private between nodes 1 and 2 from any behaviour of node 3.

However, it does not prevent node 2 to perform an action ``c''
which should be used only to communicate between nodes 1 and 3,
neither does it forbid node 1 to break in the communication of 
action ``b'' between nodes 2 and 3.

From the specification of the nodes themselves, I understand that such
disruptions will never occur, but I think that they should be prevented
at top-level with the |[...]| operator.

According to me, LOTOS should have a possibility to separate the
declaration of processes from the declaration of their interaction
with other processes. That would allow for more symetrical solutions
for the above problem. Something like this:

hide a, b, c in
  declare processes
    n1 := node[c,a],
    n2 := node[a,b],
    n3 := node[b,c]
  with communications
    n1 |[a]| n2,
    n2 |[b]| n3,
    n3 |[c]| n1

Don't fuss about the syntax just invented, just about the idea's
behind it. Did I just made a perfect fool of myself?

Kind regards,				Jan Rekers

J. Rekers, Department of Computer Science, Leiden University
P.O. box 9512, 2300 RA Leiden, the Netherlands
email: rekers@rulwi.LeidenUniv.nl
-- 
J. Rekers, Department of Computer Science, Leiden University
P.O. box 9512, 2300 RA Leiden, the Netherlands
email: rekers@rulwi.LeidenUniv.nl
From: alanw@bnr.ca (Alan Williams)
Newsgroups: comp.specification
Subject: Looking for info on SDL 92
Date: 29 Sep 92 12:59:58 GMT
Reply-To: alanw@bnr.ca
Organization: Bell-Northern Research, Ottawa ON Canada


I am looking for information on the new version of SDL that is under
development.  I would appreciate any information on what the changes
are, or pointer to obtaining a copy of a (draft) specification.

-- 
Alan Williams        |  Bell-Northern Research Ltd.   
(613)-765-2981       |  P.O. Box 3511 Station C      
alanw@bnr.ca         |  Ottawa, Ont. CANADA  K1Y 4H7
Xref: sparky comp.specification:440 sci.logic:1606
From: cjc@cm.deakin.OZ.AU (Chris Coomber)
Newsgroups: comp.specification,sci.logic
Subject: temporal logic tools
Date: 29 Sep 1992 04:17:36 GMT
Organization: Deakin University, Geelong, Australia
Distribution: world
NNTP-Posting-Host: galadriel.cm.deakin.oz.au


A week ago I requested whether anyone knew of a good FOL theorem prover.
I have since received many replies and obtained two good FOL theorem
provers, namely OTTER and SETHEO. 

Further my question, does anyone know the whereabouts of any tools for
constructing (and reasoning about) temporal logic?

Regards,
Chris Coomber
Newsgroups: comp.specification
From: jon@cs.washington.edu (Jon Jacky)
Subject: Re: temporal logic tools
Summary: What is SETHEO? Please post informative responses.
Keywords: Theorem proving, first-order logic, SETHEO
Organization: Computer Science & Engineering, U. of Washington, Seattle
Date: Tue, 29 Sep 92 16:37:00 GMT

In article <1a8ld0INN2cv@sol.deakin.OZ.AU> cjc@cm.deakin.OZ.AU (Chris Coomber) writes:
>
>A week ago I requested whether anyone knew of a good FOL theorem prover.
>I have since received many replies and obtained two good FOL theorem
>provers, namely OTTER and SETHEO. 
>

I know of OTTER, but what/where is SETHEO?  It would be useful to post 
a bit more information about availability, etc.

- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA

Newsgroups: comp.specification
From: vaccari@ghost.dsi.unimi.it (matteo vaccari)
Subject: Advantages of Z and VDM over Dijkstra-style specifications?
Organization: Computer Science Dep. - Milan University
Date: Tue, 29 Sep 1992 09:28:13 GMT


I am new to formal specifications, and I am wondering about
the advantages of using specification languages like Z or VDM
over the kind of program specifications described in the books
  "Predicate Calculus and Program Semantics" by E. Dijkstra,
or
  "Programming in the '90s", by E. Cohen

In those books in fact not so much attention is paid to specifications
as to proofs of correctness. Is this the main difference?


-- 
Matteo Vaccari                  tel.    +39-2-55006347
Dipartimento di Informatica     fax.    +39-2-55006348
Universita` di Milano           e-mail: vaccari@ghost.unimi.it
From: maler@pelvoux.imag.fr (Oded Maler)
Newsgroups: comp.specification
Subject: References of applications
Date: 30 Sep 92 17:23:15 GMT

I'm looking for recent references for *real* (well, as real
as possible) applications of formal verification methods  of 
reactive systems.

Thanks
-- 
===============================================================
Oded Maler, LGI-IMAG (Campus), B.P. 53x, 38041 Grenoble, France
Phone:  76635846  Fax: 76446675   e-mail: maler@vercors.imag.fr
===============================================================
Xref: sparky comp.specification.z:431 comp.software-eng:3591
From: fhd@panix.com (Frank Deutschmann)
Newsgroups: comp.specification.z,comp.software-eng
Subject: Users of Z formal specification
Date: 2 Oct 92 20:06:47 GMT
Organization: PANIX Public Access Unix & Internet, NYC

A few days ago, I posted a request to comp.software-eng asking the
basic question: "Who uses Z, and for what?" As a result of that
posting, I was directed to this newgroup and its FAQ. However, I have
not really seen any answers to my question; while many people are
interested in this question (I have recieved many requests for a
summary), I have not gotten much information. The only things I have
seen so far is that Z has been used for:
	1) IBM CICS development (most weel know, won an important
British award)
	2) Development of a Tek 'scope
	3) Transputer and other microprocessor design (microcode + HW)

Is this all that has been done with Z?  I find that hard to believe.
And the line "companies don't reveal their use of Z for
security/competitive reasons" just doesn't wash; I build trading
systems for a Wall Street house, and if we used Z, and derived any
benefit, we would tell the world.

So, once again, I ask my question: Does anybody use Z?

The original post follows....

-frank



Newsgroups: comp.software-eng
From: fhd@panix.com (Frank Deutschmann)
Subject: Z Specification Language -- Does anyone use it?
Date: Thu, 1 Oct 1992 00:41:47 GMT
Organization: PANIX Public Access Unix & Internet, NYC

I have been reading a great deal about Z, the formal specification
language recently, and I was curious if anyone out here on the net has
experience with or actively uses Z (or another formal specification
language/system) in real and/or academic projects.

I'm not real interested in Z theory, but rather I am interested in
real-world, real-project experience with Z. What sort of projects do
people actually specify in Z? Do they tend to be multi-gazillion
dollar century-long projects, or do-it-in-a-week projects, or
everything in between? How do programmers, analysts, end users, and
everyone in between react to Z?

Any thoughts?

(I'm not real interested in starting a formal spec vs. prototype
debate/brawl/war, but, on the other hand, that may actually be an
interesting thread to take up...)

-- 
-frank
(fhd@panix.com)
From: cmr02@scm.tp.ac.uk (Peter J Knaggs)
Newsgroups: comp.specification.z
Subject: Re: Z and Concurrency
Date: 3 Oct 92 10:08:40 GMT
X-Mailer: mail-news 2.0.3

With regard to the discussion on `Z and Concurrency' the other month, I
would like to bring your attention to the following:

@inproceedings{Z:Stod92,
	title=		"The Event Calculus (Formal Specification of Real
			 Time Systems by means of Diagrams and Z Schemas)", 

	author=		"Bill Stoddart and Peter Knaggs",

	booktitle=	"$5^{th}$ International Conference on Putting
			 into practice methods and tools for information
			 system design",

	address=	"University of Nantes, Institut Universitaire
			 de Technologie, 3 Rue du Mar\'echal Joffre,
			 44041 NANTES Cedex 01, France",

	month=		sep,

	year=		1992}

I do have a copy of this paper in LaTeX format, although we do intend
re-write parts of it as a result of comments received during the
conference.

--
Peter J. Knaggs.       School of Computing and Maths, University of Teesside,
pjk @ scm.tees.ac.uk   Middlesbrough, Cleveland, England.    +44 (642) 342673
-----------------------------------------------------------------------------
        C makes you think that C is the world's greatest language.
    Forth makes you think that you're the world's greatest programmer.
-----------------------------------------------------------------------------
Ps: Having just completed my PhD Thesis, I am on the lookout for any good
    jobs.  Please contact me if you know of any.
From: Michael.Hinchey@cl.cam.ac.uk (Michael Hinchey)
Newsgroups: comp.specification.z
Subject: Re: Z and Concurrency
Date: 3 Oct 92 13:28:29 GMT
X-Mailer: mail-news 2.0.3


   
dsd

Dear Dr. Knaggs,

I have read your message on Z-forum, and am very interested in your
paper.  I would have liked to attend that conference in Nantes, but
unfortunately it clashed with the submission of my M.Sc.

I am just starting my Ph.D. here at Cambridge.  I haven't sorted out
the exact area that I will be working in as yet, but it will be to
do mainly with integrating structural design and formal methods 
(specifically Z), and theorem provers (Isabelle).  As my M.Sc. dealt
with real-time systems, I am thinking of looking in particular at
how combinations of the above could be used in reactive systems.

Your paper would therefore be of great interest to me.  Would it
be possible to get a LaTeX copy of it; or will the proceedings be
published in the near future?

Thank you for your time.

Regards,

-- Mike.
.

-----------------------------------------------------------------------------
Michael G. Hinchey

University of Cambridge Computer Laboratory,		St. John's College,
New Museums Site,					CAMBRIDGE,
Pembroke Street,					CB2 1TP,
CAMBRIDGE,						England.
CB2 3QG,
England.


	Voice	: +44-223-332400	(Laboratory)
		  +44-223-334420	(Direct)

	Fax	: +44-223-334678

	e-mail	: Michael.Hinchey@cl.cam.ac.uk
		  HINCHEYM@ul.ie
		  hincheym@itdsrv1.ul.ie
From: mbenveni@irisa.fr (Marc Benveniste)
Newsgroups: comp.specification.z
Subject: Z for Word-5 anyone?
Date: 29 Sep 92 07:09:44 GMT
Organization: IRISA, Rennes (Fr)

Anyone knows how to write Z specifications with Word-5
in the PC world ?

Any suggestions as how to do it ?

Thanks in advance.

--Marc.
___________________________________________________
Marc Benveniste          tel: (33)      99.84.72.93
IRISA                    FAX: (33)      99.38.38.32
Campus de Beaulieu        @ : mbenveni@irisa.fr
35042 Rennes Cedex
FRANCE.
From: cliff@cs.man.ac.uk (Cliff B Jones)
Newsgroups: comp.specification
Subject: Re: Advantages of Z and VDM over Dijkstra-style specifications?
Date: 30 Sep 92 08:59:40 GMT
Organization: Dept Computer Science, University of Manchester, U.K.

In article <1992Sep29.092813.19695@ghost.dsi.unimi.it> vaccari@ghost.dsi.unimi.it (matteo vaccari) writes:
>
>I am new to formal specifications, and I am wondering about
>the advantages of using specification languages like Z or VDM
>over the kind of program specifications described in the books
>  "Predicate Calculus and Program Semantics" by E. Dijkstra,
>or
>  "Programming in the '90s", by E. Cohen
>
>In those books in fact not so much attention is paid to specifications
>as to proofs of correctness. Is this the main difference?

Z and VDM have evolved from "straight predicate calculus"
specifications as the need to specify larger systems has been
understood. Both Z and (the specification language part of) VDM employ
a collection of data types which make it easier to build abstract
models of systems.

It is certainly *not* true that VDM (the method) pays less attention
to proofs although I would emphasize their use in development rather
than post facto correctness proofs. See for example

	
@book{Jones90a,
	author	    =	"C. B. Jones",
	title	    =	"Systematic Software Development using VDM",
	edition =	{Second},
	publisher   =	"Prentice Hall International",
	year	    =	"1990",
	length =	"333 pages"
}

@book{JonesShaw90,
	editor =	"C. B. Jones and R. C. F. Shaw",
	title =		"Case Studies in Systematic Software Development",
	publisher =	"Prentice Hall International",
	year =		"1990",
	length =	"387 pages"
}

The situation with Z on development is more complex: the early books
were confined to specifications (and proofs about the specifications
themselves); more recently, many people use Morgan's "refinement
calculus".

An interesting discussion on the use of Z/VDM is in Hoare's Preface to


@book{VDM90,
	editor =	"D. {Bj\o rner} and C. A. R. Hoare
			and H. Langmaack",
	title =		"{VDM'90: VDM and Z} -- 
			Formal Methods in Software Development",
	publisher =	"Springer-Verlag",
	year =		1990,
	volume =	428,
	series =	"Lecture Notes in Computer Science"
}


cliff jones
Newsgroups: comp.specification
From: martin@weigele.de (Martin Weigele)
Subject: Re: Z information
Organization: M. Weigele
Date: Tue, 29 Sep 1992 20:24:57 GMT

In article <22467@venera.isi.edu> donc@isi.edu (Don Cohen) asks about  
references on the Z specification language.

There is a newsgroup comp.specification.z with monthly faq-postings.

-- 
Martin Weigele, Kapellenweg 32, D-W-5300 Bonn 2
phone +49 228 333252 home, +49 228 9866385 office
email: martin@weigele.de
From: cjc@cm.deakin.OZ.AU (Chris Coomber)
Newsgroups: comp.specification
Subject: SETHEO details
Date: 30 Sep 92 00:08:59 GMT
Article-I.D.: sol.1aar6rINNgnj
Distribution: world
Organization: Deakin University, Geelong, Australia
NNTP-Posting-Host: galadriel.cm.deakin.oz.au

For those wanting to know more about the FOL theorem prover SETHEO, here
is the information that was sent me recently.


----------------------------------------------------------------------------

We (the Artificial Intelligence Research Group `Intellektik' at the Chair of
Computer Architecture of the Technical University in Munich) have heard that 
you are interested in our 

			  High Performance Theorem Prover

				*** S E T H E O ***

After several new developments concerning SETHEO and its components 
we are now able to provide a modified and updated set of the sources 
of SETHEO for the UNIX operation system. 

They can be obtained via FTP in the following way

	% ftp 131.159.8.35	(or "ftp flop.informatik.tu-muenchen.de")

	Name: anonymous
	Password: <your-e-mail-address>

	ftp> binary
	ftp> cd pub/fki
	ftp> get setheo.readme.first
	ftp> get setheo.tar.Z
	ftp> bye


The commands above will download the two files setheo.readme.first and
setheo.tar.Z to your local machine.  (The file setheo.readme.first gives 
advise about how to unpack the sources contained in the file setheo.tar.Z.
Included are also two Postscript files with papers concerning SETHEO.)

Alternatively you can order a tape containing the SETHEO sources
for a fee of US$ 50,- from the following address:

 Max Moser (or Klaus Mayr)
 Institut fuer Informatik		 
 Technische Universitaet Muenchen
 Postfach 20 24 20
 Arcisstr. 21	
 D-8000 Muenchen 2
 Germany


In case of problems please contact `setheo@informatik.tu-muenchen.de'
or write to the address above. The e-mail address above will also be your
future contact address for requests, inquiries, ... .


Good Luck,
	and much fun with
	
		SETHEO
From: esj@harvee.billerica.ma.us (Eric S Johansson)
Newsgroups: comp.specification
Subject: Re: Advantages of Z and VDM over Dijkstra-style specifica
Date: 2 Oct 92 01:03:48 GMT
Reply-To: esj@harvee.billerica.ma.us
Organization: gators 'r us
X-Software: HERMES GUS 1.03 Rev. Apr 14 1992

In <1992Sep29.092813.19695@ghost.dsi.unimi.it>, matteo vaccari writes:
>
>I am new to formal specifications, and I am wondering about
>the advantages of using specification languages like Z or VDM
>over the kind of program specifications described in the books
>  "Predicate Calculus and Program Semantics" by E. Dijkstra,
>or
>  "Programming in the '90s", by E. Cohen

I think the major advantage Z/VDM have over the Dijkstra methods is
that Z/VDM have a better PR machine.  Any formal technique is so
much better that the way software is developed now that it really
doesn't matter which one you use as long as the notation is a good fit
to your task.

>In those books in fact not so much attention is paid to specifications
>as to proofs of correctness. Is this the main difference?

The Dijkstra methods focus more on developing an appropiate notation
(one that fits your task), elegant solutions in a mathamatical sense,
and a checkable proof.  These methods do *not* imply you can
prove anything correct.  I guess the best you can hope for is a
correct proof and derivation of code.

--- eric
-- 
HOME: esj@harvee.billerica.ma.us  HAM  ka1eec
WORK: 617.630.4687 (w)   esj@ruby.polaroid.com
source of the public's fear of the unknown since 1956
Newsgroups: comp.specification