news@cs.mu.oz.au (news) (09/27/89)
From: sharam@munnari.oz.au (Sharam Hekmatpour) Path: munnari.oz.au!sharam A number of people have recently asked for copies of EPROS. I thought this might of interest to others as well: EPROS is an environment that supports VDM and a lot more. Using it, you can write VDM specifications, fully check their syntax and semantics, and compile them into executable code. It also includes a C-like programming notation, dialogue notation, meta abstraction, etc. The source for EPROS is available free of charge. The official user manual for the system is: S. Hekmatpour and D. Ince, Software Prototyping, Formal Methods and VDM, Addison-Wesley, Wokingham, 1988 (hardback). To obtain a copy of EPROS, ftp (anonymous) to: munnari.oz.au (178.250.1.21) the source is in: pub/epros.tar.Z To build the system you need a C compiler + Franz Lisp on a UNIX machine. Instructions for building the system are included with the source. ------------------------------------------------------------------------- sharam@munnari.oz.au Dept. of Computer Science, Melbourne University, Parkville, Victoria, Australia 3052. -------------------------------------------------------------------------
cdornan@acorn.co.uk (Chris Dornan) (10/09/89)
As was pointed out to me many times, I meant Z when I said VDM in my original posting. At last, here is the summary of tools available for Z and VDM. Unfortunately, much work seems to be going on in research projects in large companies, behind closed doors. I have had the basic information for at least a week but chasing people for minor details such as a contact point for ordering have held things up. Note, in the features section, I have given an indication of features that I am reasonably sure are applicable to the system in question. This list is far from complete and there will be features missing -- check out properly any systems that look as if they could be appropriate, regardless of features not listed here. N.B. # = pounds sterling Fuzz - Mike Spivey Notation - Z Price - Sun #300 PC #200 Features - type Setting, syntax checker, type checker Hardware - Sun 3, IBM PC Comments - Takes LaTex sources as its input. Order information from: mike@prg.ac.oxford.uk EPROS - Melbourne University Notation - VDM Price - Free Features - source code, syntax checker, type checker, animation Hardware - Unix machine running Franz Lisp See also - comp.software-eng: <2197@munnari.oz.au> 'Genesis' - IST, Cambridge, U.K. Notation - Z Price - ~#4,000 Features - editor included, syntax checker, type checker, proof checking Hardware - Sun 3 Order information - 3 Glisson Road, Cambridge, UK (UK) 0223 462400 Comments - The toolset arose from the 'Genesis' project but the tools themselves may be called something else. FORSITE - Racal Research Notation - Z Price - ? Features - WYSIWYG editor (including postscript printing facilities) syntax checker, type checker, cross referencer, schema expander, helper Hardware - Sun 3 Comments - FORESITE was developed under an Alvey project. FORESITE is now in use in Racal. It is expected that FORESITE will be made available in the near future. If interested, please contact Andrew Rickets, Racal Research Ltd. tel +44 734 868601 ext. 300 Specbox - Adelard Notation - VDM Price - PC AT #995 PC 386 #1,495 Sun 3 #3,000 (Single User, provisional) #7,500 (2-5 Users, provisional) Features - BSI draft standard, full static checking, modules, test harness Hardware - now: PC AT, PC 386 soon: Sun 3/4 and VAX/VMS Order information - Peter Froome 28, Rhondda Grove London E3 5AP -- Chris Dornan Acorn Computers Limited, Fulbourn Road, Cherry Hinton, Cambridge. cdornan@acorn.co.uk