HDTenEightyP/NetNews huggingface dataset:
From: andre@iesd.auc.dk (Atte Andre Jensen)
Newsgroups: comp.music
Subject: Hard-disk recording
Date: 1 Apr 92 14:38:00 GMT
Distribution: comp.music
Organization: Mathematics and Computer Science, Aalborg University


Hi

I'm considering buying equipment for harddisk recording for my Atari
ST. I need (at least) the following requirements to be met:

  o Accaptable sound-quality (sample-rate above 40 KHz)

  o At least 4 tracks (more are fine with me)

  o The system must not exclude my other programs to run on the Atari
    (not talking 'bout multitasking, and I don't know if this would be
    a problem)

I expect the HD-recording-"system" to be a combination of soft- &
hardware.

Have any of you experience with any system in paticular?
Recomendations & critiques are wellcome.

Thanx in advance...


--


                                 Atte Andre Jensen
                                (andre@iesd.auc.dk)
            Department of Computer-Science, Aalborg University, Denmark
Newsgroups: comp.music
Subject: Re: FTP sites for cool NeXT apps
From: zazula@bonehead.tucson.az.us (Ralph Zazula)
Date: 6 Apr 92 03:33:52 MST
Distribution: world,local

In article <1992Apr1.101003.15503@mailer.cc.fsu.edu>  writes:
> Would someone please either post or E-Mail me a list of FTP
> sites for NeXT music apps (you know, all the real cool public
> domain stuff, that MIT, Princeton, Columbia guys and anybody
> who's anybody is working on or has completed).
> 
Check these two out:

	ccrma-ftp.stanford.edu
	princeton.edu

Ralph

--
 |------------------------------------------------------------------|
 | Ralph Zazula                           "Computer Addict!"        |
 | University of Arizona                                            |
 | NeXT Campus Consultant                                           | 
 | zazula@bonehead.tucson.az.us           (NeXT Mail)               |
 |------------------------------------------------------------------|
From: little@cs.ucsd.edu (Glenn Little)
Newsgroups: comp.music
Subject: Re: Steinberg Cubase problem
Date: 13 Apr 92 17:49:19 GMT
Organization: CSE Dept., UC San Diego


In article <1992Apr10.113317.11506@issun3.stc.nl>, koelman@cuby.stc.nl (Ton Koelman) writes:
|> In article <hjv.702814111@groucho.phil.ruu.nl> hjv@phil.ruu.nl (Hendrik  
|> Jan Veenstra) writes:
|> > Stewart.Lawler@f634.n712.z3.fx.cec.edu.au (Stewart Lawler) writes:
|> > 
|> >
|> > 
|> > >I have Cubase version 2.1 (running on a 1meg Atari ST) which has
|> > 
|> > I know this isn't any help, but alas... I've never seen a program crash  
|> as much
|> > as Cubase, so I don't think your enthusiasm (or anybody else's) is  
|> justified.
|> > Cubase has a lot of nice features (and misses some (IMHO) very important
|> > features :), but the Steinberg-people should take a few

  
  What are some of the things Cubase users find missing?  What would
  you like changed?  What bugs have you found (not just on the Atari...
  I'm using the mac version myself).  I've started making a list of
  things I'd like to bring to their attention, and would like to
  make it complete.  Perhaps if I got the list to the american St. Jones
  rep, and one of our European users got the list to the European rep,
  there would be more chance of some of our concerns being addressed.
  As a lone user, I just feel that my concerns aren't all the noticable,
  especially when you consider that they have to be filtered through the
  American people to the developers in Europe.

		-glenn
		glittle@ucsd.edu
Organization: Freshman, Math/Computer Science, Carnegie Mellon, Pittsburgh, PA
Newsgroups: comp.music
Date: Sat, 11 Apr 1992 23:04:59 -0400 
From: Philip Andrew Nemec <pn0q+@andrew.cmu.edu>
Subject: Re: GRAVIS ULTRASOUND -- NEW INFO (Long!)

Excerpts from netnews.comp.music: 9-Apr-92 GRAVIS ULTRASOUND -- NEW IN..
by David DeBry@itchy.dsd.es 
> - Includes MIDI In, Out, Thru connectors

    Does the MIDI conform with Sound Blaster Midi, or it's own, or
something standard like MPU?

                        Philip Nemec
Xref: sparky comp.music:2394 rec.music.synth:7857 bit.listserv.emusic-l:687
From: siffert@ucsu.Colorado.EDU (Thunder-Thumbs)
Newsgroups: comp.music,rec.music.synth,bit.listserv.emusic-l
Subject: Cadenza for Windows
Date: 11 Apr 92 22:09:00 GMT
Article-I.D.: ucsu.1992Apr11.220900.24361
Organization: University of Colorado, Boulder

I want to buy Cadenza for Windows, and the price I've seen around
here is for $300.  Does anyone know where I can get it for cheaper,
or does anyone know of a better sequencing program for the IBM
(comparable to the best Mac programs)?  And could you also quote
the price for me, if known?

Finally, I have heard that one can get a demo for cadenza somewhere
on ftp, does anyone know where?  Thanks.

Thunder-Thumbs
 


-- 
*  Curt Siffert                  *  'In the heart of the rain forest, it  * 
*  Thunder-Thumbs                *   was doing what it usually does in    *
*  maestro@boulder.colorado.EDU  *   rain forests; which is rain; hence   * 
*  Paper-Mache Cows Forever...   *   the name.'  - Douglas Adams          *
From: hjv@phil.ruu.nl (Hendrik Jan Veenstra)
Newsgroups: comp.music
Subject: Re: Steinberg Cubase problem
Date: 14 Apr 92 10:38:16 GMT
Organization: Department of Philosophy, University of Utrecht, The Netherlands

little@cs.ucsd.edu (Glenn Little) writes:

>  What are some of the things Cubase users find missing?  What would

- An easy way to record and manually edit Sys-Ex messages. I *need* to
be able to hex-edit Sys-Ex and still haven't found out how this can be done in
Cubase (if it's possible at all).
- A serious possibility for 'thinning out controllers'. The fixed algorithm
Cubase now uses ('do-it-our-way-or-don't-do-it-at-all') is absolutely useless
for a serious composer who happens to use (sometimes) a lot of controller data.
- A way to define sections -i.e. parts of existing tracks- which can then be
'chained' to create a new track. But these sections should be 'ghost-sections',
i.e. they should take NO memory/they should not be real copies of the original,
but merely pointers to the original, so that when you edit the original, the
copy in the chain is also changed (because it's the same data). This makes it
possible to create 'mega-complex' patterns without using up all your available
memory.
- A better implementation of the Master Track. First of all, tempo and meter
changes should be separated (different tracks) - after all, tempo and meter are
two totally different things, aren't they? So why are they put on one track
anyway? It should be possible to maintain different meter and tempo tracks at
the same time (although only one of each can be active at a time (of course))
Since music depends a lot on accelerandos and ritenutos and since electronic
music tends to get to 'stiff' due to quantising and since editing a tempo track
(in order to get rid of this 'stiffness') is tedious, boring and
time-consuming, it should be possible to add tempo-changes in a flexible way,
e.g. by using an on-screen slider while the music is playing.
- A way to stretch and compress tracks (so that e.g. 4 beats get compressed to
1 1/3 beat).

Well, guess that's enough for the moment. When I discovered some of the above
shortcomings, I decided to buy another sequencer which has all the desired 
abilities...:)
I *may* be wrong on some of my critiques - I haven't used Cubase -that- much
(for obvious reasons), so it is possible that some of the above missing
features are in fact possible, but that I just haven't discovered them yet (and
probably will not discover them either :).












































--
Hendrik Jan Veenstra - Department of Philosophy
University of Utrecht - The Netherlands
USENET: hjv@phil.ruu.nl   * don't worry about life; it's not permanent *
From: macrakis@osf.org (Stavros Macrakis)
Subject: Formal description of Unix interface and internals
Organization: OSF Research Institute
Date: 8 Apr 92 13:55:51

I'm interested in formal specifications of the external interface
(API) and the internal interfaces of Unix.  By internal interfaces, I
mean especially the invariants of critical data structures such as
vnodes, the process structure, etc.

Can anyone point me in the right direction?  Please reply by E-mail,
and I will summarize.

Thanks,

	-s

Stavros Macrakis
Open Software Foundation Research Institute

Mail:  11 Cambridge Center, Cambridge, MA 02142, USA
Net:   macrakis@osf.org
Phone: + 1 / 617 / 621 8892 (direct, voicemail)
Fax:   + 1 / 617 / 225 2943
Xref: sparky comp.specification:177 comp.software-eng:1745 comp.theory:1049
From: jon@cs.washington.edu (Jon Jacky)
Newsgroups: comp.specification,comp.software-eng,comp.theory
Subject: Re: Seeking verification condition generators
Summary: Here are two references, a book and a paper
Keywords: preconditions, postconditions, program correctness
Date: 7 Apr 92 16:07:30 GMT
Organization: Computer Science & Engineering, U. of Washington, Seattle

This book describes a solution in Lisp for a Pascal-like language.  In 
addition to the VC generator, it also presents the theorem prover:

@book{gordon88,
        author="Michael J.C. Gordon",
        title="Programming Language Theory and its Implementation: Applicative
                and Imperative Paradigms",
        publisher="Prentice Hall",
        year=1988}

A shorter article on the topic is:

@article{gray87,
        author="D. Gray",
        title="A Pedagogical Verification Condition Generator",
        journal="The Computer Journal",
        volume=30,
        number=3,
        year=1987,
        pages="239 -- 248"}

Jonathan Jacky                      jon@radonc.washington.edu
Radiation Oncology RC-08            (206)-548-4117 voice
University of Washington            (206)-548-6218 fax
Seattle, WA 98195
USA
From: esj@harvee.UUCP (Eric S Johansson)
Newsgroups: comp.specification
Subject: Re: formal methods in US
Date: 10 Apr 92 06:48:02 GMT
Distribution: comp.specification
Organization: gators 'r us
X-Version: Rodney's UUCP modules 02/11/90 V1.18

In article <1992Mar31.164952.18327@beaver.cs.washington.edu> jon@cs.washington.edu
(Jon Jacky) writes:

> In article <1992Mar31.015456.2392@oracorp.com> narayana@oracorp.com (K. T. Narayana) writes:
> > I would appreciate if people cut off this half baked survey of people
> > working in formal methods in north america. 
> > ...kt
> 
> In contrast, I would like to say that I have found this interesting and do 
> appreciate seeing it, and would welcome additional contributions.   It's easy
> enough for people to skip over articles that do not interest them.
> 
> - Jon Jacky, Radiation Oncology RC-08, University of Washington, Seattle USA

I too have found this communication interesting and I have been
entertaining thoughts of it degenerating into a comp.specification.aa
meeting (my name is eric and I am a coder :-) 

This discussion is dealing (indirectly) with change.  How do I get {
myself, my manager, my coworkers, ... } to change to understand and 
hopefully use formal methods.  by understanding what we learn, how we
learn it and what motavates us to learn formal methods, we can convince
others and know what to teach them.  In trying to change my work environment
I have encountered indifference, hostility, fear and far too little
excitement.  

more later.  it's past time to go to work.

--- eric
--
UUCP ...!uunet!wang!harvee!esj esj@harvee.uucp  HAM  ka1eec
WORK AT&T (617) 577-4068 (w)   johansson@athena.polaroid.com
source of the public's fear of the unknown since 1956
Newsgroups: comp.specification.z
From: jon@cs.washington.edu (Jon Jacky)
Subject: Greek letters in schema names and FUZZ
Summary: How can I do it?
Keywords: Z, FUZZ, framing, promotion, phi
Organization: Computer Science & Engineering, U. of Washington, Seattle
Date: Mon, 13 Apr 92 21:38:07 GMT

Does anyone know how to get FUZZ to accept schema names that have capital Greek
letters in them?

Some classic Z case studies do this.  In particular, the Unix file system paper
by Morgan and Sufrin (IEEE TOSE SE-10(2), March 1984, also reprinted in the
Hayes Case Studies book) introduced the convention of including the capital
Greek letter Phi in the names of framing schemas.   I like that, but I can't
figure out how to do it.  Here is an example of my problem:

Say I have a framing schema that I pronounce "S frame T".   I can spell it out
just that way:

\begin{schema}{SFrameT}
        x: \nat %  Just a dummy
\end{schema}

But, I'd like to spell it S<insert capital Phi here>T.

Here are some attempts to insert the "Phi" in the name of the framing schema:

\begin{zed}
        S\PhiT \defs SFrameT
\also
        S \Phi T \defs SFrameT
\also
        S{\Phi}T \defs SFrameT
\end{zed}

None of these work.  The first attempt doesn't even get past LaTeX, which
complains:

        ! Undefined control sequence.
        l.44 ^^IS\PhiT
                       \defs SFrameT
        ?

... and only the capital letter S appears in the printed output.  The other two
are accepted by LaTeX, and the printed output looks just as I intended. But,
for all three alternatives, FUZZ issues the same error message, for example:

        "phi.tex", line 28: Syntax error at symbol `\defs'

Am I missing something that is obvious to LaTeX adepts, or are such schema
names just not permitted with FUZZ?

Also, is it possible to have hyphens in schema names?  For example, S-Frame-T.
LaTeX/FUZZ sees these as minus signs.  I know about underscores, but hyphens
are used in the case studies book, and some people prefer them.

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: khb@informatik.uni-kiel.dbp.de (Karl-Heinz Buth)
Newsgroups: comp.specification.z
Subject: refinement notions in Z and VDM
Keywords: refinement, Z, VDM
Date: 9 Apr 92 08:50:16 GMT
Organization: Dept. of Computer Science, University of Kiel, FRG

Currently, I am investigating the relation between the refinement
notions in VDM and Z. After having read Cliff Jones' book on VDM and
Mike Spivey's reference manual on Z, it seems to me that there is not
much of a difference. After translation into the other formalism, the
proof obligations look essentially the same. Since I am not so very
experienced in Z, I would like the Z community to comment on this. Am
I right, or are there fundamental differences between Z and VDM in
this area?

I know that there has been quite some discussion on Z vs. VDM on the
net during last year. But this was mostly on other aspects like
usability, and not so much on theoretical foundations.


Karl-Heinz Buth
+--------------------------------------------------------------+
|  Institut fuer Informatik, Christian-Albrechts-Universitaet  |
|          Preusserstr. 1-9, W-2300 Kiel 1, Germany            |
|        Tel.: ++49-431-560421  Fax: ++49-431-566143           |
|   E-mail: khb@causun.uucp, khb@informatik.uni-kiel.dbp.de    |
+--------------------------------------------------------------+
From: asathaye@galley.ece.cmu.edu (Archana Sathaye)
Newsgroups: comp.specification.z
Subject: Archive Files for "Formal Methods for Specification"
Date: 13 Apr 92 15:50:19 GMT
Article-I.D.: fs7.1992Apr13.155019.22654
Organization: Electrical and Computer Engineering, Carnegie Mellon


Hi, 

I saw a note indicating where the archives files for the
discussion on "formal methods for specification" are located.
It was mentioned that the files are on lth.se in
pub/netnews/specification. My question is,

"What Log-in do I use to get on to lth.se"?
I tried "anonymous" (username and password) and
"guest" and it did not work.

Could someone out there please let me know, how I
get to these files?


                                    Thanks,
                                    Archana
From: I.C.L.Hol@win0109.wins.icl.co.uk
Newsgroups: comp.specification.z
Subject: ICL Proof Tool Newsletter
Date: 6 Apr 92 17:21:24 GMT
X400-Received: by mta eros.uknet.ac.uk in /PRMD=UK.AC/ADMD=GOLD 400/C=GB/;
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5); Relayed;
X400-Originator: I.C.L.Hol@uk.co.icl.wins.win0109
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000013400000012]
Original-Encoded-Information-Types: undefined
X400-Content-Type: P2-1984 (2)
Content-Identifier: 12
Original-Message-Id: <"12*/I=ICL/S=Hol/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
X-Mailer: mail-news 2.0.3


         ICL PROOF TOOL for HOL and Z (and SAL, and modal logics....)

         The second newsletter on the above topic has recently been
         distributed to most of those who asked to be put on the
         distribution list.

         I was unable to get the newsletter through to the following
         people:

              David Carrington
              Paul Jackson
              Sara Kalvala
              Ludwig Hausen

         whose addresses may have changed since the first newletter, could
         they possibly offer me an up-to-date address?

         Any new readers of info-hol or comp.specification.z who would like
         to receive the above newsletter should send either (or all of) an
         email address, a fax number or a postal address to:

              I.C.L.Hol@win0109.uucp
         or   I.C.L.Hol@win0109.wins.icl.co.uk

         or to:

              R.B.Jones
              International Computers Limited
              Eskdale Road
              Winnersh
              Wokingham
              Berks RG11 5TT
              England
Newsgroups: comp.specification
From: kayaalp@seas.smu.edu (Mehmet M. Kayaalp MD)
Subject: Archieve site of comp.specification
Organization: School of Engineering and Applied Science
Date: Thu, 9 Apr 1992 15:21:21 GMT


Could you please let me know, if there is any archieve site of this newsgroup.
I missed the discussions on Formal Methods. If any of you saved that, could you
send it to me ( I esp. need the references )  

Thank You in advance for your help!
Best regards,
mehmet

-- 
Mehmet M. Kayaalp, M.D.         phone  : (214)692-3095
Computer Science Department     voice  : (214)706-5982
Southern Methodist University   fax    : (214)692-3085
Dallas, Texas 75275-4191        E-mail : kayaalp@seas.smu.edu
From: jon@cs.washington.edu (Jon Jacky)
Newsgroups: comp.specification
Subject: Re: formal methods in US
Summary: Formal methods likened by some to Alcoholics Anonymous, etc.
Date: 13 Apr 92 17:35:06 GMT
Distribution: comp.specification
Organization: Computer Science & Engineering, U. of Washington, Seattle

In article <4521577@harvee.UUCP> esj@harvee.UUCP (Eric S Johansson) writes:
>
> I have been entertaining thoughts of (this thread) degenerating into a 
> comp.specification.aa meeting (my name is eric and I am a coder :-) 
>

At a workshop on formal methods in the USA a few years ago, one computer
scientist got up and said, "I don't really consider myself part of this 
community.  It seems like you (the formal methods community) are a bit like
Alcoholics Anonymous or Weight Watchers - you are trying to get people to 
do this difficult thing that will reform and improve them."

That's a not uncommon view of formal methods in the USA, I think.

Jonathan Jacky                      jon@radonc.washington.edu 
Radiation Oncology RC-08            (206)-548-4117 voice
University of Washington            (206)-548-6218 fax
Seattle, WA 98195	
USA
Newsgroups: comp.specification
From: macrakis@osf.org (Stavros Macrakis)
Subject: Re: What is the situation of FM outside Europe?
Organization: OSF Research Institute
	<1992Mar25.192454.2627@gdr.bath.ac.uk>
Date: 8 Apr 92 13:46:27

In article <1992Mar25.192454.2627@gdr.bath.ac.uk>
masljg@gdr.bath.ac.uk (L J Groves) writes:

   I doubt that you'll find anything else like MCC in the US....  It caused quite
   an uproar at the time, because the kind of cooperative, industry-funded
   research that the 5GP was based on was simply not possible under US law...

Such cooperative, industry-funded research could well have been an anti-trust
violation earlier, because the law defined certain kinds of activities as
anti-competitive (violation of anti-trust law) regardless of their real effect on
competition.  But the National Cooperative Research Act of 1984 provided a legal
framework for this kind of cooperation, and MCC was (I think) the first to take
advantage of its provisions.  The NCRA was of course passed in response to
Japanese (and perhaps also European) cooperative research programs.

Since then, other organizations have been formed under the NCRA, including the
Open Software Foundation (OSF).  I believe that the Software Productivity
Consortium and the Petroleum Open Software Corporation were also formed under
this act.

	-s

Stavros Macrakis
Open Software Foundation Research Institute

Mail:  11 Cambridge Center, Cambridge, MA 02142, USA
Net:   macrakis@osf.org
Phone: + 1 / 617 / 621 8892 (direct, voicemail)
Fax:   + 1 / 617 / 225 2943
 
Xref: sparky comp.specification:175 comp.software-eng:1733 comp.theory:1046
From: dsims@leo.ece.uc.edu (David Sims)
Newsgroups: comp.specification,comp.software-eng,comp.theory
Subject: Seeking verification condition generators
Keywords: preconditions, postconditions, program correctness
Date: 6 Apr 92 14:42:54 GMT
Organization: University of Cincinnati, ECE Department

Hello,

I'm looking for software tools or references to papers that address
verification condition generators (program correctness condition
generators).  My literature search to date has come up empty :(

Given a program annotated by axiomatic style verification conditions
(preconditions and postconditions), this tool will extract each
precondition/postcondition pair (possibly using the "weakest precondition"
function) and send it to a theorem prover.  If the theorem prover verifies
all the assertions sent to it by the verification condition generator,
then the program has been proved correct.

Such a tool will avoid reproving assertions that were already proved.  It
might make other optimizations as well.

***

Pointers to references or tools for any programming language would be
greatly appreciated.


Thanks,

David Sims
dsims@thor.ece.uc.edu
Newsgroups: comp.specification
From: kayaalp@seas.smu.edu (Mehmet M. Kayaalp MD)
Subject: test
Organization: School of Engineering and Applied Science
Date: Thu, 9 Apr 1992 15:25:03 GMT


-- 
Mehmet M. Kayaalp, M.D.         phone  : (214)692-3095
Computer Science Department     voice  : (214)706-5982
Southern Methodist University   fax    : (214)692-3085
Dallas, Texas 75275-4191        E-mail : kayaalp@seas.smu.edu 
Newsgroups: comp.specification
From: kayaalp@seas.smu.edu (Mehmet M. Kayaalp MD)
Subject: test
Organization: School of Engineering and Applied Science
Distribution: dfw
Date: Thu, 9 Apr 1992 15:29:00 GMT

test

-- 
Mehmet M. Kayaalp, M.D.         phone  : (214)692-3095
Computer Science Department     voice  : (214)706-5982
Southern Methodist University   fax    : (214)692-3085
Dallas, Texas 75275-4191        E-mail : kayaalp@seas.smu.edu
From: collberg@dna.lth.se (Christian S. Collberg)
Newsgroups: comp.specification
Subject: Re: Archieve site of comp.specification
Date: 12 Apr 92 16:52:11 GMT
Article-I.D.: lth.1992Apr12.165211.2189
Organization: Department of Computer Science, Lund University

In article <1992Apr9.152121.17563@seas.smu.edu> kayaalp@seas.smu.edu (Mehmet M. Kayaalp MD) writes:
>
>Could you please let me know, if there is any archieve site of this newsgroup.
>Best regards,
>mehmet

comp.spcification is archived at "lth.se" in pub/netnews/specification.

Christian



-- 
Christian.Collberg@dna.lth.se
Department of Computer Science, Lund University, BOX 118, S-221 00 LUND, Sweden
Newsgroups: comp.specification
From: kayaalp@seas.smu.edu (Mehmet M. Kayaalp MD)
Subject: test
Organization: School of Engineering and Applied Science
Distribution: tx
Date: Thu, 9 Apr 1992 15:26:51 GMT

test

-- 
Mehmet M. Kayaalp, M.D.         phone  : (214)692-3095
Computer Science Department     voice  : (214)706-5982
Southern Methodist University   fax    : (214)692-3085
Dallas, Texas 75275-4191        E-mail : kayaalp@seas.smu.edu 
Xref: sparky comp.specification:184 comp.software-eng:1775