HDTenEightyP/NetNews huggingface dataset:
From: Jim.Davies@prg.ox.ac.uk (A Wooden Fish on Wheels)
Newsgroups: comp.specification.z
Subject: Re: Z and concurrent systems
Date: 18 Aug 92 14:15:51 GMT
	<JIM.DAVIES.92Aug14175257@pierrot.prg.ox.ac.uk>
	<1992Aug17.170419.23826@dscomsf.desy.de>
Organization: Foundations for the Laboratory of Computer Science, Oxford
In-reply-to: hallam@zeus02.desy.de's message of 17 Aug 92 17:04:19 GMT


In article <...> hallam@zeus02.desy.de (Phillip M. Hallam-Baker) writes:

   If you are looking for a useful calculus then it might be a good idea to
   start by observing that both CSP and Z are already pretty complex
   systems. 

I disagree.  

The Z notation is simpler than any other formal method I can think of.

The theory of CSP isn't that difficult to understand. 

Didn't someone like Einstein say that a theory should be "as simple as
possible, but no simpler"?  What's the use of switching to an easier 
calculus or method if it's no longer adequate?

   Combining them is asking to produce something so mind boggling
   huge and vast that most people will move to something rather smaller of
   their own devising.

It's the "divising" part that's the complicated bit.  I'm (reasonably) happy
to rely upon the skills of aircraft engineers when I fly; I don't expect to
build my own plane.  And that's more complicated than booking a ticket and
flying.  It's a bit of a useless analogy, but I'm sure you get the point. 

Just because we had to think in metric spaces in order to check that the
language and models of CSP were all hunky dory, it doesn't mean that you need
to know anything more than basic set theory in order to use them.  I'm sure
that a similar argument applies to Z...

Jim




--
Xref: sparky comp.specification:377 comp.specification.z:399
From: cant@itd.dsto.gov.au (Tony Cant)
Newsgroups: comp.specification,comp.specification.z
Subject: Genesis Z-Tool
Keywords: Specification languages, Tool support
Date: 20 Aug 92 17:04:33 GMT
Reply-To: cant@itd.dsto.gov.au
Followup-To: comp.specification.z
Organization: Defence Science and Technology Organisation

I would like to know if anyone out there has experience in using the 
 Genesis Z-Tool, distributed by Imperial Software Technology (UK).
 We have been using  Version 2 (Jan 1992), and have
 encountered problems understanding the proof tool.   The main
problem is the connection between the syntax-directed editor  and the 
Common Lisp interface, and, especially, writing tactics in Lisp.

 If anyone can show us some worked examples of proofs using tactics,
 or point to any articles  or any other material which would help us
 understand this  proof tool,  it  would be greatly appreciated.
 
We have experience with both HOL and Isabelle, so understand the
general ideas and techniques involved in goal-directed proofs using tactics.


Thanks,

Dr Tony Cant
Trusted Computer Systems Group
Information Technology Division
Defence Science and Technology Organisation
SALISBURY South Australia
(cant@itd.dsto.gov.au)
Newsgroups: comp.specification
From: csds@alpha.ru.ac.za (David Sewry)
Subject: Formal Specifications in CCS
Keywords: CCS
Organization: Rhodes University, Grahamstown, South Africa
Date: Wed, 12 Aug 1992 13:30:44 GMT


Hello

I am using Milner's CCS to specify the Linda programming model.
(This work forms part of a larger project which aims to construct
a parallel debugger.)

I am keen to learn of any efforts in the use of CCS as a specification
tool, or its use in the specification of such parallel paradigms.

(I have also posted this to comp.parallel.)

David Sewry
Internet: csds@alpha.ru.ac.za
Newsgroups: comp.specification
From: Lamport@src.dec.com
Subject: Re: Linear and Branching Time Temporal Logic
Followup-To: Lamport@src.dec.com
Keywords: TLA, Temporal Logic of Actions
Organization: DEC Systems Research Center
Date: Fri, 21 Aug 92 23:05:56 GMT

In article <172o80INNk2k@iraul1.ira.uka.de>, zundel@i10s7 (Armin Zundel) writes:

|> after reading some papers about temporal logic I had some problems to
|> decide when to use linear time logics and when to use branching time
|> logics. I decided to read 
|> 
|> "Sometimes" and "Not Never" revisited: On Branching versus Linear Time
|> Temporal Logic 
|> by E.a. Emerson and J.Y. Halpern.
|> 
|> Now I'm even more confused. I just want so specify distributed systems.
|> Can anyone tell me what real life properties can be specified with
|> linear time logic and which can be specified in branching time logic. 


Dear Mr. Zundel,

Your message will probably stimulate lots of philosophical debate among
theoreticians.  Here's my view, based on my experience actually
verifying and specifying concurrent systems.  

The simplest linear-time logic, with just state predicates and the Box
operator, can express the intuitive concepts "always" and "eventually".
The analogous branching-time logic, with just state predicates and the
Box operator, can express the intuitive concepts "always" and
"possibly".  Since "eventually" is a pretty important concept, I don't
think anyone advocates the use of such a simple branching-time logic.
I believe that the branching-time logics that people propose allow one
to express both "eventually" and "possibly".  I have never wanted to
write a specification such as

  "If the user enters an input, then it is possible for the system to
   produce the correct answer."

so the ability to express possibility is of no interest to me.
Therefore, I've found linear-time temporal logic adequately expressive,
and have no need for complicated branching-time logics.

Unfortunately, a simple linear-time logic with just Box and state
predicates isn't expressive enough.  You need something more.  The
traditional approach has been to add more powerful temporal operators,
and to write a specification as a list of temporal-logic formulas.
However, my experience is that, for systems of any complexity, such
specifications become incomprehensible and are usually wrong.  The only
practical specification methods are ones that write a specification as
an abstract program.  (Petri nets and CCS formulas are examples of
abstract programs.) However, programs aren't as mathematically simple
or as amenable to manipulation and reasoning as logical formulas are.

My approach is to use just the Box operator, but to generalize from
simple state predicates to predicates on pairs of states.  With this
logic, which I call TLA (the Temporal Logic of Actions), it is easy to
write abstract programs as logical formulas.  For example, one could
express the program that starts with x equal to 0 and repeatedly
increments x by one as

   (x = 0)  /\  [](x' = x+1)

(where /\ denotes conjunction and [] denotes Box).  TLA is described in
a research report that I am sending you in a separate message.

Leslie Lamport
From: agoodloe@gmuvax2.gmu.edu (Alwyn Goodloe)
Subject: Sigplan article
Organization: George Mason University, Fairfax, Va.
Distribution: comp.specification
Date: Sat, 15 Aug 1992 02:24:21 GMT

 In the July 1992 Sigplan Notices Aidan Ward of Coherent Technology Ltd.
describes a toolset for supporting formal development of programs called
BluePrint.  Does anyone know if this is really a real development
project. If so, what is the specification language going to look like.


Alwyn E. Goodloe
agoodloe@gmuvax2.gmu.edu
Newsgroups: comp.specification
From: lagemaat@cs.utwente.nl (Jeroen van de Lagemaat)
Subject: Re: parallel programming and specification tools
Organization: University of Twente, Dept. of Computer Science
Date: Thu, 13 Aug 1992 08:17:47 GMT

In article <1992Aug12.150936.16184@porthos.cc.bellcore.com>, haim@dancer.uucp (24103-kilov) writes:
|> 
|> "Besides, the crucial thing about Formal Methods is "What tool support is
|> available" - and be suspicious of "tools" as well!! There are few real good
|> ones."
|> 
|> Absolutely not! A formal method is used to understand what you are talking
|> about, i.e., to specify the "system" better. If, as a result of its use,
|> the specification has less errors and/or is more complete and understandable,
|> then it does not really matter whether there exists a miraculous tool that,
|> with a push of a button, will create code out of a specification.
|> 
|> -Haim Kilov
|> haim@dancer.cc.bellcore.com
|> 

Absolutely YES. For trivial systems one may think that writing it down in
a formal methods will allow one to capture the whole problem. For less
simple cases one needs tools to be able to reason about the specification.

Examples: - Syntax and static semantics checkers (nearly allows very experienced
            people make such mistakes, but why spend time on it if a computer
            can help us)
          - Animator or simulator, to animate the behaviour we have written
            down to check our assumptions about the specifications
          - Verification to check whether some properties hold (more
            difficult than animation to make tools because of the inherent
            complexity
          - Report generators, to get a better overview (e.g. graphical
            representation).

Finally compilation will be great, but one must not forget that also bridging 
the gap between first specification (of user-requirements generally) and the
final implementation in hard/software, a lot of human intelligence is needed.

So for thousands of centuries we can learn that the human kind is capable 
of making and using tools, but still we need humans to do both.


    ___
 __/   \__________  Jeroen van de Lagemaat    <lagemaat@cs.utwente.nl>
|  \___/          |         
|___     __   ___ | University of Twente     
| |  |  /  \ (__  | Tele-Informatics & Open Systems
| |__|__\__/____) | P.O. Box 217  NL-7500 AE Enschede  The Netherlands
|_________________| tel. +31 53 893684              tfx. +31 53 333815

                    Humour, you're making me laugh.
                                    - Herman Finkers, Dutch comedian -
From: charlot@sun3.lri.fr (Francois Charlot)
Newsgroups: comp.specification
Subject: For Steve Austin - Sorry for the others
Date: 14 Aug 92 17:24:48 GMT
Reply-To: charlot@sun3.lri.fr (Francois Charlot)
Organization: LRI - Univ. Paris-Sud / CNRS URA 410

I'm sorry for all the users of this newsgroup, but we have some troubles
to send mails (and perhaps not too much to receive some ?).
I would like to send this to Stephen Mark Austin <sma@seg.npl.co.uk>,
but our Mailer-Daemon seems to be on strike. I'll try not to 
repeat this too much.

Thanks for your comprehension.



Dear Steve,

  Actually, if I wanted this request, it was not really to
answer, but to see what kind of questions you wanted us to
answer (both for educational and industrial purposes). That is,
I'm more interested in the results of your request. As you
perhaps read in the news, I have to deal with formal methods
and I don't know yet what I'm going to do.

Sincerely,

	Francois.

-- 
+--------------------------+------------------------------------+
|                          |    E-mail : charlot@lri.lri.fr     |
|     Francois CHARLOT     |             charlot@FRLRI61.BITNET |
|                          |                                    |
|        +-=-+-=-+         |    Tel    : 33 - 1 - 69 41 70 82   |
|                          |    Fax    : 33 - 1 - 69 41 65 86   |
+--------------------------+------------------------------------+
|      ######      **                                           |
|     ##     #         Laboratoire de Recherche en Informatique |
|    ##       #   ##   Batiment 490                             |
|   ##       #   ##    Universite de Paris-Sud                  |
|  ##    ####   ##     91405 ORSAY CEDEX                        |
| ######    ## ##      FRANCE                                   |
|######      ###                                                |
+---------------------------------------------------------------+
From: berstel@mipsmath.math.uqam.ca (Bruno Berstel)
Newsgroups: comp.specification
Subject: Where is Verilog ?
Date: 20 Aug 92 18:44:31 GMT
Reply-To: berstel@lacim.uqam.ca (Bruno Berstel)
Organization: Universite du Quebec a Montreal

[English follows]

Bonjour,

J'aimerais bien connaitre une adresse electronique de ceux qui sont
derriere Veda. L'entreprise qui vend la license s'appelle Verilog.
J'aimerais exposer les bugs que je crois avoir trouve dans Veda, savoir
comment obtenir les corrections et plus si affinite :-).

Merci d'avance,
   Bruno.

Hello,

I would like to get in touch (via email) with the people who wrote and
maintain Veda. The company is Verilog.
I'd like to talk about the bugs I think I have found in Veda, the patches
for them and even more.

Thanks in advance,
   Bruno.
-- 
-----     -----     -----     -----     -----     -----     -----     -----
Bruno Berstel                                         berstel@lacim.uqam.ca
Laboratoire de Combinatoire et d'Informatique Mathematique       L.A.C.I.M.
Universite du Quebec a Montreal                                    U.Q.A.M.
(Tele)phone : (514) 987-8495                           Fax : (514) 987-8477
---------------     ---------------     ---------------     ---------------
                    Noel en hiver, Paques au printemps.
Newsgroups: comp.specification
From: haim@dancer.uucp (24103-kilov)
Subject: Re: parallel programming and specification tools
Reply-To: haim@dancer.UUCP ()
Organization: Bellcore, Livingston, NJ
Date: Wed, 12 Aug 92 15:09:36 GMT


"Besides, the crucial thing about Formal Methods is "What tool support is
available" - and be suspicious of "tools" as well!! There are few real good
ones."

Absolutely not! A formal method is used to understand what you are talking
about, i.e., to specify the "system" better. If, as a result of its use,
the specification has less errors and/or is more complete and understandable,
then it does not really matter whether there exists a miraculous tool that,
with a push of a button, will create code out of a specification.

-Haim Kilov
haim@dancer.cc.bellcore.com

Newsgroups: comp.parallel
From: jjackson@carlrs6000.carl.ua.edu (Jeff Jackson)
Subject:  RPC usage in FORTRAN on distributed SUN workstations. 
Organization: The University of Alabama
Date: Tue, 11 Aug 1992 20:09:42 GMT

I have two questions.

 1) What manual(s) describes the FORTRAN usage of Remote Procedure Calls?
    I have all the SUN manuals, including the Network Programming Guide,
    but all examples there are in C.  My code must be F77 (arrrrgghh!).

 2) I have heard (via a previous post that I no longer have) that PVM
    (availability?) may help me.  If so, what is PVM, what will it do for
    me, and where can I get it?

Please email any response to jjackson@tiger.carl.ua.edu or
jjackson@carlserver.carl.ua.edu.

Thanks in advance.

Jeff

-------------------------------------------------------------------------------
David Jeff Jackson                         Internet: jjackson@tiger.carl.ua.edu
Electrical Engineering Dept.                                    (130.160.48.25)
P.O. Box 870286
The University of Alabama                The Computer Architecture Research Lab
Tuscaloosa, AL 35487-0286
Phone: (205) 348-2919
-------------------------------------------------------------------------------

Newsgroups: comp.parallel
From: pgraham@silver.cs.umanitoba.ca (Peter Graham)
Subject: Wanted: Public Domain parallel machine simulators
Apparently-To: comp-parallel@math.waterloo.edu
Organization: Computer Science Dept., University of Manitoba, Winnipeg, Canada
Distribution: na
Date: Mon, 17 Aug 1992 18:42:15 GMT

I am interested in getting pointers to free parallel machine simulators for
use in a 4th year undergraduate honours course which surveys parallel
systems. I used the Blitzen(/MPP) simulator last term with reasonable
success and would like to expand the students' experience to include other
such systems representing other types of parallel machines. I would greatly
appreciate any advice/comments/suggestions people may have. (Particularly
those which relate experiences in a similar academic setting.) My thanks
in advance.     Peter
---
Peter C.J. Graham			<pgraham@cs.umanitoba.ca>
Computer Science			(204) 474-8313
University of Manitoba, Winnipeg MB
Canada R3T 2N2

Newsgroups: comp.parallel
From: basak@news.cis.ohio-state.edu (Debashis Basak)
Subject: Info on clustered architectures.
Organization: The Ohio State University Department of Computer and Information Science
Date: Thu, 13 Aug 1992 20:17:58 GMT

Hi,

I am interested to get some references to papers on clustered architectures,
by which I  mean a distributed memory  architecture with supernodes arranged
in some regular topology, where each supernode is a cluster of processors 
with shared memory/distributed memory, e.g. a mesh of meshes.

I am willing to post a compilation of the responses.

Thanks in advance.

-Debashis Basak
 basak@cis.ohio-state.edu



Newsgroups: comp.parallel
From: hojungc@cs.man.ac.uk (Hojung Cha)
Subject: Crossbar switching chips - info needed
Reply-To: hojungc@cs.man.ac.uk (Hojung Cha)
Organization: Department of Computer Science, University of Manchester UK
Date: 12 Aug 92 14:37:21 GMT


Apology if this is much out-of-date question.

As part of our multiprocessing hardware project, we are looking 
for some commercially available bit-parallel crossbar switching 
chips. So far we've found a couple of such chips; for instance, 
AMD's Am29C983 Multiple Bus Exchange chip and TI's 74ACT8841 
(I heard that the TI chip is now obsolete). Are there other such 
chips available in the market (or in the research lab) ?  
Any response will be much appreciated.

Regards,
Hojung Cha

--
-------------------------------------------------------------------
Hojung Cha
Dept. of Computer Science          Phone    : +44 61 275 6255
University of Manchester           Fax      : +44 61 275 6236
Manchester M13 9PL, U.K.           E-mail   : hojungc@cs.man.ac.uk
-------------------------------------------------------------------

Newsgroups: comp.parallel
From: ojuarez@mtecv2.mty.itesm.mx (Octavio Juarez Espinosa)
Subject: Looking info about shared memory systems
Summary: Help
Keywords: Shared memory systems
Organization: I.T.E.S.M. Campus Monterrey
Date: 12 Aug 92 13:59:46 GMT





Hi,

I am very interested in to receive some information about shared memory
systems (parallel).

I'll appreciate if give some references about programming paradigms for
parallel architectures.

Thanks in advance.

Sincerely,

Octavio Juarez Espinosa
ojuarez@mtecv2.mty.itesm.mx

-- 
Octavio Juarez Espinosa
Gabriel Valerio 1134 
Saltillo, Coahuila    CP 25000
Mexico  email ojuarez@mtecv2.mty.itesm.mx

Newsgroups: comp.parallel
From: steve ("Steve" Stevenson)
Subject: Student Volunteers needed for Supercompting
Organization: Clemson University
Date: Tue, 18 Aug 92 13:55:03 -0400

[I got this through other sources...don't respond to me]

               *** ATTENTION STUDENTS ***

>From the Student Volunteer Committee of SUPERCOMPUTING'92:
> 
...........................................................................
> Student volunteers are needed for the SUPERCOMPUTING '92 conference to be 
> held in Minneapolis in November, 1992.  Volunteer positions will require 
> from 25 to 30 hours of duty during or prior to the conference from Thursday, 
> November 12, to Friday, November 20.  Every effort will be made to design 
> their duty schedule so that they can attend some conference activities of 
> their choice, including a tutorial, technical sessions, minisymposia, 
> workshops, etc.
> 
> Students selected by the SC'92 Student Volunteer Committee to work at 
> Supercomputing '92 will receive the following benefits:
> 
>      o   Complimentary Registration & Banquet Activities
>      o   Hardcopy of Conference Proceedings
>      o   Free hotel room (double occupancy) during the time you are 
>          assisting at SUPERCOMPUTING '92.
>      o   Complimentary admittance and handouts for one tutorial.
> 
> Any student enrolled in an undergraduate or graduate program may apply by 
> completing the application form and returning it as soon as possible.
> 

Since the SUPERCOMPUTING'92 committee is not providing financial support
for students to travel to Minnesota, the North Carolina Supercomputing 
Center will provide students from North Carolina Institutions who are 
selected as volunteers by the SC'92 student volunteer committee with a 
$100 Travel Grant (up to 10 students, first come first served), in order 
to encourage students to volunteer to work at this educational event.

For an application form, get the anonymous ftp file 

        "/pub/general/sc92volunteer.info" 

from ncsc.org (or send email to info@ncsc.org requesting a form).

Application forms are due by Friday, August 28, 1992.
=======================================================================
The '92 volunteer program will reward you with an enriching conference 
experience and provide you with special opportunities to learn more 
about advanced computing and its applications.  
                                 ###


Newsgroups: comp.parallel,comp.sys.super,comp.unix.aix
From: chcho@vnet.ibm.com ( Chul-hee Cho )
Subject: Re: SupEur 92 Conference Announcement
Apparently-To: <comp-parallel@uunet.uu.net>
News-Software: UReply 3.0
Organization: IBM
Disclaimer: This posting represents the poster's views, not those of IBM
Date: Thu, 13 Aug 92 12:05:50 KST

>                     ========================
>                     SUPERCOMPUTING IN EUROPE
>                     ========================
>
>                  INVITATION AND FINAL PROGRAM FOR
>
>                    ==========================
>                         SUPEUR 92, Umea
>                      September 13-16, 1992
>                    =========================
>

Hi !  I am a novice to this newsgroup.
I like to know if there's plan for comparable session to be held
in the U.S.  - by SUPER! (?) .


Newsgroups: comp.parallel
From: lycmit@x1sun6.ccl.itri.org.tw (Yin-Chih Lin)
Subject: Where to find the IBM 3090 console emulator for Sun/IBM PC?
Organization: Clemson University
Date: Wed, 12 Aug 92 11:19:49 CST

Greetings:

I would like to apologize in advance, if this is the wrong place to
post this mesage.

We just try to connect the Sun SPARCstations and IBM PCs to the 
IBM 3090 machine (50 miles away) through TCP/IP interconnections.
We can telnet/ftp to this IBM machine, however, some packages on
the machine required the 3090 console mode.

We try to figure out the ways for tailoring our workstations and PCs
to simulate the 3090 consoles, but fail. So we think, maybe someone
out there have the similar experience and would be kind enough to 
drop us the notes.

I recalled that some Supercomputer centers in USA did install the
IBM 3090 models (such as Cornell National Supercomputer Facility).
So I suppose maybe someone in these units did connect the Sun
workstations and IBM PC to their 3090 machines.

Any directions will be appreciated, please forward your notes to me
directly.

Thanks,


------------------------------------------------------------------------------
Yin-Chih Lin                   Industrial Technology Research Institute (ITRI)
Design Eng.                    Computer & Communication Research Labs.  (CCL)
lycmit@x1sun6.ccl.itri.org.tw  Microcomputer System Department X100

Newsgroups: comp.parallel