Article View: comp.specification
Article #275Re: Specification v. design languages (was Re: Goals, Cost, and Flexibility)
From: Bernard Berthomieu,28c,6408
Date: Fri, 16 Oct 1992 09:19
Date: Fri, 16 Oct 1992 09:19
115 lines
5525 bytes
5525 bytes
In article 11643@topaz.comlab.ox.ac.uk, bowen@prg.ox.ac.uk (Jonathan Bowen) writes: >In article <Bw4MuE.8GL@exnet.co.uk> dhd@exnet.co.uk (Damon) writes: >>In article <1992Oct14.040754.14470@CS.ORST.EDU> >> crowl@jade.CS.ORST.EDU (Lawrence Crowl) writes: >>> >>>.... > >>SML, on the other hand, even though it is not completely characterised, >>is much nearer the mark and can actually execute too. Quite quickly in >>fact, since what optimisations are permissible can be worked out... > >Yes, SML is great for prototyping, and may be fast enough in practice >as well for some applications. But it is executable (you have to think >about *how* it is going to run, not just *what* you want to do), so it >is not ideal for specification. And non-deterministic specifications >which allow the designer freedom of choice in certain aspects of the >design which need not be fixed at the specification stage are of course >impossible. > >>CCS is a great spec language for concurrency. Might make a good >>parallel asm language. > >CCS (and CSP) are great *design* languages if you are targeting >your implementation onto a parallel system. You may also want to >think about the system at a more abstract level (e.g., at the >requirements stage). > >>In fact I've done CCS -> SML -> C, but actually demoed the SML in >>real-time for a network router. > >Great! I'd be interested to hear about the mapping from CCS to SML. >Can this (was this) undertaken in a rigorous and systematic manner? > >-- > >-- >Jonathan Bowen, <Jonathan.Bowen@comlab.ox.ac.uk> >Oxford University Computing Laboratory. I'm taking the opportunity to place an announcement for the latest release of LCS, a programming language based upon SML and CCS. In addition to core SML capabilities, LCS allows one to declare and run CCS-extended behaviors. It also provides facilities for monomorphic user overloadings. The standard ftp distribution notice follows. Bernard Berthomieu. (address at the end of the message) ====================================================================== Summary of features: LCS (a Language for Communicating Systems) is designed as an extension of core Standard ML with behaviors and processes based upon an high order extension of Robin Milner's CCS formalism. Behaviors are defined in an SML framework as values of specific types, which may be turned into processes. LCS supports all constructions of CCS, plus behavior passing, computed communication lines, support of side effects (both strong and light processes) and an exception mechanism at process level. Specific behavior types assign possibly polymorphic types with every communication labels. Two user interfaces are provided: an Execution interface and a Simulator. In addition to the capabilities of a Standard ML environment, the LCS executive adds those of defining behaviors and managing processes created from these behaviors. The simulator allows the user to control the expansion of a behavior, with tracing of communications. The simulator helps to debug LCS programs, it also makes a valuable tool for teaching or learning CCS. LCS is implemented as a byte code interpreter; it is reasonnably fast and robust. Binaries and core image files are small, core images are portable accross machines. ---------------------------------------------------------------------- The ftp distribution: LCS V3.1 is available for Sun3 and Sun4 workstations, under SunOS 4. It may be obtained by ftp anonymous on site laas.laas.fr (140.93.0.15), directory /pub/lcs; or by streamer tape, on request. The ftp distribution is constituted of the following files: README directives for installation V3-1.tar.Z libraries, man pages and miscellaneous doc.tar.Z users manual and other reports bin.tar.Z core image files for all targets sun3_4.1.1.tar.Z binaries for SUN3 under SunOS 4.1.1 sun4_4.1.1.tar.Z binaries for SUN4 under SunOS 4.1.1 Set binary mode; copy files README, V3-1.tar.Z, doc.tar.Z, bin.tar.Z and the binary file(s) for your machine(s) and operating system(s); install as explained in file README. ---------------------------------------------------------------------- The mailing list: mail: for: lcs-request@laas.fr registration/deletion to the lcs list lcs@laas.fr contributions to the lcs list lcs-bugs@laas.fr bug reports bernard@laas.fr any other reasons ---------------------------------------------------------------------- Contact: Bernard Berthomieu LAAS-CNRS, 7, Avenue du Colonel Roche, F-31077 Toulouse Cedex e-mail: bernard@laas.fr phone: (+33) 61 33 64 08 fax: (+33) 61 55 35 77 The LCS project is partially supported by CNRS/Greco C-Cube.
Technical Details
Message-ID:
<7923@laas.laas.fr>Path:
arc1-ca.pugleaf.net!sparky!uunet!europa.asd.contel.com!gatech!swrinde!cs.utexas.edu!sun-barr!ames!agate!doc.ic.ac.uk!uknet!mcsun!corton!laas!ava!bernardReferences:
<1992Oct15.090326.11643@topaz.comlab.ox.ac.uk>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!europa.asd.contel.com!gatech!swrinde!cs.utexas.edu!sun-barr!ames!agate!doc.ic.ac.uk!uknet!mcsun!corton!laas!ava!bernard From: bernard@ava.laas.fr (Bernard Berthomieu,28c,6408) Newsgroups: comp.specification Subject: Re: Specification v. design languages (was Re: Goals, Cost, and Flexibility) Message-ID: <7923@laas.laas.fr> Date: 16 Oct 92 09:19:21 GMT References: <1992Oct15.090326.11643@topaz.comlab.ox.ac.uk> Sender: news@laas.fr Reply-To: bernard@ava.laas.fr Organization: LAAS-CNRS, Toulouse (France) Lines: 115 Nntp-Posting-Host: ava