VDM

Vienna Development Method

Version: 1.3

A Japanese version of this FAQ now exists and is maintained by Takanori Ugai (ugai@syslab.iias.flab.fujitsu.co.jp). It will be distributed by him through fj netgroups (Japanese NetNews). A copy can also be obtained by anonymous ftp from: sa-ftp.cs.titech.ac.jp:/pub/VDM

Both the English and Japanese versions can be retrieved from: - the Mailbase archives (mailbase.ac.uk, 128.240.2.118) > - by anonymous ftp: ftp.ifad.dk (130.255.136.3) in /pub/vdm

A LaTeX version of this FAQ is being finalised, and can be retrieved from these archives shortly.

Subject: Index

1. What is VDM?
2. Where are the other VDMers?
3. Where can I find papers on VDM?
4. Where do I start learning about VDM?
5. What is the semantics of VDM-SL?
6. What Modularity is provided in VDM?
7. I heard there's a Standard for VDM...
8. Does VDM support object-orientation?
9. Can VDM handle concurrency?
10. Is VDM executable?
11. What is data reification?
12. How is VDM related to algebraic specification languages?
13. How does VDM compare to Z?
14. What is the relationship between VDM and RSL?
15. What is the relationship between VDM and the Refinement Calculus?
16. Who is using VDM?
17. What sorts of system can VDM be used to describe?
18. What tools are available?
19. There's something missing from this FAQ! Whom do I tell?
20. References

Subject: What is VDM?

VDM stands for "The Vienna Development Method": a collection of techniques for the formal specification and development of computing systems. It consists of a specification language called VDM-SL; rules for data and operation refinement which allow one to establish links between abstract requirements specifications and detailed design specifications down to the level of code; and a proof theory in which rigorous arguments can be conducted about the properties of specified systems and the correctness of design decisions.

The term "VDM" is sometimes used a little carelessly to mean the specification language only.

VDM's origins lie in the research on formal semantics of programming languages at IBM's Vienna Laboratory in the 1960s and 70s, including the VDL and Meta-IV notations. VDM is their modern descendent, now used well beyond the bounds of language semantics in industrial systems development as well as academic research. A number of other specification languages extend or were inspired by VDM-SL, including RSL, VVSL and VDM++ (all mentioned below). VDM-SL is now in the final stages of standardisation by ISO. See [HJN93] for a brief review of VDM's history.

VDM-SL is a model-oriented specification language. This means that a specification in VDM-SL consists of a mathematical model built from simple data types like sets, lists and mappings, along with operations which change the state of the model. For example, a specification of a hotel reservation system would contain a mapping from room numbers to names and addresses of occupants (modelled as character strings), along with operations to add and remove guests and rooms, occupation dates etc. Basic types like Natural numbers, characters, and type constructors like sets and maps, are provided "for free" in VDM-SL.

In the rest of this FAQ, you will find discussions of VDM and its extensions, how it relates to other formalisms, where it has been used and how to get more information, including The VDM Bibliography and Standard, introductory texts, tool support, industrial usage and courses.

Subject: Where are the other VDMers?

Well, about 200 of them subscribe to the vdm-forum, which is a low-traffic electronic mail list for problems, tips and techniques on specification & refinement; information about tools, conferences, courses; reports on public industrial and academic projects; VDM-SL semantics, proof theory and the standardisation effort. To subscribe, send an email message to mailbase@mailbase.ac.uk containing the following line alone in the message body:

join vdm-forum <YourName>

e.g.

join vdm-forum John Fitzgerald

The list is unmoderated, but is administered by John Fitzgerald at the University of Manchester (John is vdm-forum-request@mailbase.ac.uk). Contact him if you have any problems or questions about joining or using the list. Please remember, however, that he is not a system administrator, and acts only in a voluntary capacity.

You can meet real live VDMers at many conferences, especially the Formal Methods Europe (FME) symposium held every 18 months. The FME symposia started as VDM-specific gatherings, which widened to embrace the entire range of formal techniques.

FME is a European organisation, supported by the European Union, with the mission of promoting and supporting the industrial use of formal methods. As well as the FME symposium, the group organises seminars to introduce potential industrial users to the ideas of formal methods and the benefits that other industrial users have achieved by using them. Contact the FME Committee Secretary Tim Denvir, Translimina Ltd, 37 Orpington Road, Winchmore Hill, London N21 3PD, UK (E-mail: timdenvir@cix.compulink.co.uk).

The British Computer Society's special interest group on Formal Aspects of Computing Systems (BCS FACS) contains a number of VDMers. Along with FME, BCS FACS publishes a joint newsletter called "FACS Europe" which includes an occasional VDM column. Contact: BCS FACS, Department of Computer Science, Loughborough University of Technology, Loughborough, Leicestershire, LE11 3TU, UK (E-mail: FACS@lut.ac.uk).

Subject: Where can I find papers on VDM?

You can find papers on VDM in Journals such as IEEE Transactions on Software Engineering, The Software Engineering Journal, Formal Aspects of Computing, The Computer Journal, Acta Informatica, Science of Computer Programming and many others. The VDM Bibliography lists hundreds of papers, books and reports on VDM from a wide variety of sources. It's available by anonymous ftp from:

> ftp.ifad.dk in directory /pub/docs

chopwell.ncl.ac.uk in directory /pub/vdm_bibliography

ftp.imada.ou.dk in directory /pub/docs

If you have World-wide Web access, you can get The Bibliography, Standard and lots more via the VDM Home Page:

> http://www.ifad.dk/vdm/vdm.html

Subject: Where do I start learning about VDM?

The following introductory books have been recommended by people other than their authors!

C B Jones "Systematic Software Development using VDM" Prentice Hall International ISBN 0-13-880733-7, 2nd Edn. 1990

J Dawes "The VDM-SL Reference Guide" Pitman/UCL Press ISBN 0-273-03151-1, 1991

D Andrews and D Ince "Practical formal methods with VDM" McGraw Hill ISBN 0-07-707214-6, 1991

J T Latham, I D Cottam and V Bush "The Programming Process: an introduction using VDM and Pascal", Addison Wesley, 1990

The VDM Bibliography has a much more comprehensive list, and indicates which books are more suited to advanced users.

There are many courses on VDM. A few of these are listed below:

Manchester University's Department of Computer Science (PEVE Unit) offers a range of courses on VDM, including a five-day offering covering specification, refinement and proof in VDM, including the use of a formal reasoning support system. A three-day introductory version and a one-day intensive course are also available. Contact Ursula Hayes or Helen Sheehy - Tel +44 (0)61 275 6172; Fax +44 (0)61 275 6172; E-mail: uhayes@cs.man.ac.uk or hsheehy@cs.man.ac.uk.

VDM courses are available from Adelard: length of training courses vary from a one day overview, though an intensive 5 days, and as long as 2 to 3 weeks when clients want a significant case study of their choosing to be undertaken. Adelard's SpecBox VDM checker tool is used on the courses. Training on a client's own premises is the norm, but other venues are possible. Contact Ian Cottam in the Manchester office - Tel +44 (0)61 861 7399, or Peter Froome in the main London office - Tel +44 (0)81 983 1708.

VDM courses are also offered by IFAD, the Institute of Applied Computer Science. A five-day training course as well as a three-day intensive course, both with hands-on experience, are available. The training course includes an introduction to formal methods; an introduction to the concepts and notation used in VDM; and exercises covering the use of the IFAD VDM-SL Toolbox. Courses specially tailored to a company or application area can be arranged. Contact Peter Gorm Larsen - Tel +45-63-157131; Fax: +45-65-932999; E-mail: peter@ifad.dk

Icon Computing (Europe) offer a Workshop on Rigorous Object Oriented Design. This short, informal, exercise-driven course introduces the application of VDM-based techniques in object-oriented analysis and design. The aim is a practical level of rigour, providing a precise language of behaviour for documenting and discussing requirements, abstract classes, and system composition from re-usable components. Contact: Alan Wills, Icon Computing Europe Ltd., Tel: +44 (0)161 257 3292, Fax: +44 (0) 161 225 3240, Email: info@icon.demon.co.uk

Praxis plc offer a 4-day course on VDM. The course is divided into several different modules, each covering different aspects of VDM. Each module is followed by a tuturial. The final day is spent on a case study; an English requirements specification has to be specified using VDM. By the end of the course, attendees should be able to understand and write small VDM specifications. As prerequisites, attendees should have experience in high level programming languages, such as Pascal. A minimum background in mathematics such as British A-Level or that associated with a university degree is required, along with some fluency in set theory and logic. (This can be gained from Praxis' 2-day 'Discrete Mathematics For Software Engineering' course). Contact: Mike Greenan or Anthony Hall, Praxis plc, 20 Manvers Street, Bath, AVON, BA1 1PX, UK , Tel: +44 225 444700, Fax: +44 225 465205, Telex: 445848 PRAXIS G, Email: mpg@praxis.co.uk

Subject: What is the semantics of VDM-SL?

VDM-SL has a formally defined semantics. The logic underlying this semantics is based on the Logic of Partial Functions (LPF) [BCJ84,C86,CJ91,JM94]. The definition of the semantics is given in a denotational style in the VDM-SL Standard. Recursive definitions are given a least fixed point semantics. Definitions given in VDM-SL can be loose (have different functionality) and therefore a syntactic VDM-SL specification will, in general, denote a (infinite) set of models.

The semantics are given in the VDM-SL draft Standard. See the section on "I heard there's a Standard for VDM..." in this FAQ for details of the Standard.

Subject: What Modularity is provided in VDM? 

A good VDM-SL specification will be carefully structured: related pieces of text will be grouped together and will intersperse explanatory text. "Modules" in the "heavyweight" programming language sense (with parameters, imports, exports and information hiding) are not present in the ISO Standard Language. This is because users of VDM-SL haven't yet found there is enough need for this facility to have it standardized. A movement towards this is growing, however. A number of tools (e.g. Adelard's SpecBox and IFAD's VDM-SL Toolbox) and authors (e.g. [M93,F91]) define module mechanisms. If you want to structure your large specifications, you should use a tool which supplies a facility for this anyway. For further reading, look at the section on "Structuring" in The VDM Bibliography.

Subject: I heard there's a Standard for VDM... 

The specification language part of VDM (VDM-SL) is currently being standardised under auspices of the ISO and British Standards Institute. Currently, the standard is a Committee Draft. It is hoped to become a Draft International Standard within the next six months or so, and make it to full International Standard in 1995.

You can get a copy of the Standard by anonymous ftp from the following sites. Please use the one nearest to you:

The United Kingdom: Denmark: chopwell.ncl.ac.uk ftp.imada.ou.dk in directory /pub/vdmsl_standard in directory /pub/vdmsl_standard

The USA: The Netherlands: gatekeeper.dec.com dutiba.twi.tudelft.nl in directory /pub/standards/vdmsl in directory /pub/vdmsl_standard

Australia: ftp.cs.uq.oz.au in directory /pub/vdmsl_standard

Again, if you have World-wide Web access, you can get The Standard, Bibliography and lots more via the VDM Home Page:

> http://www.ifad.dk/vdm/vdm.html

Subject: Does VDM support object-orientation?

Two extensions of VDM support object-orientation:

VDM++, developed as part of the ESPRIT project Afrodite (Project No. 6500), extends Standard VDM-SL with object-oriented constructs and concurrency. Real-time extensions are planned for the future. VDM++ is supported by a toolset with a graphical user interface (VDM++ checkers, a code generator, facilities for pretty-printing), linked to a tool from which it is possible to (partially) generate a VDM++ specification from a graphical OMT model. Further details are in [DvK92], [DP94] and [DGP94]. Contact Nico Plat, Cap Volmac, Dolderseweg 2, 3712 BP Huis ter Heide, The Netherlands (E-mail: Nico.Plat@ACM.org).

Fresco provides a VDM-like environment for developing SmallTalk applications on the basis of formal methods. Specifications and proofs serve to drive and to structure software development and are integrated with the code for documentation purposes. The system allows a "rigorous" approach, with the user free to choose the level of formality. Fresco is supported by a Fresco/SmallTalk interpreter, the mural theorem prover and a graphical browser. References are [Wills91,92,94]. Contact: Alan C. Wills, Icon Computing Europe Ltd, 24 Windsor Road, Manchester M19 2EB, UK (Tel: +44 (0)61 225 3240, E-mail: alan@cs.man.ac.uk).

Subject: Can VDM handle concurrency?

A number of approaches have been worked out for handling concurrency in VDM, none of these having (yet) achieved the level of use needed to make it part of the ISO Standard VDM-SL.

In systems where part of the state might be changed by several processes, classical post-conditions aren't enough to fully express an operation's functionality. This comment applies to other formal methods as well.

One approach to extending VDM-like specifications for concurrency adds rely-/guarantee-conditions as a way of specifying and reasoning about interference. The initial work on this is reported in [Jon81], the best reference is [Jon83]; more recent work includes [Sto90], [Xu92] and [Col94].

Other approaches include the "inter" condition in VVSL [M93] and concurrent object-oriented ways of controlling and reasoning about interference [Jon93], and work in VDM++[DGP94].

For further reading, look at the section on "Concurrency" in The VDM Bibliography.

Subject: Is VDM executable?

You can write executable and non-executable specifications in VDM-SL. The pros and cons of executing specifications have been discussed in [HJ89], [F92], [A+92] and [L94].

A number of researchers have developed execution facilities for VDM-SL subsets (or closely-related dialects). Most of these have transformed specifications into programs in a programming language (see the section on "Prototyping" in The VDM Bibliography). Recently, direct interpretation of VDM-SL specifications has been implemented (see the section on VDM tools in this FAQ).

Subject What is data reification?

Data reification is the VDM terminology for what most other people would call data refinement - that is, the taking of a step towards an implementation by replacing a data representation without a counterpart in the intended implementation language (such as sets) by one that does have a counterpart (such as maps with fixed domains, which can be implemented by arrays), or at least one which is closer to having a counterpart, such as sequences. The word "reification" is preferred over "refinement" because the process has more to do with making an idea concrete than with making it more refined.

A reification step can only be taken if it can be guaranteed that the behaviour of the reifying definition will be the same as that of the original definition as far as the users of that definition are concerned. The data reification proof obligations of VDM [Jones90, appendix E.3] are sufficient to establish this when the "user" is another VDM specification, but they are known not to be complete: that is, some definitions with the same behaviour cannot be justified as implementations using them. [Jon90] discusses complete generalizations: [Cl92] does the same at greater length and in a wider setting. [Nip86] (the source for the generalisations) emphasizes the importance of what can be observed in justifying reification conditions, and proposes alternative sets of conditions for different situations.

Subject: How is VDM related to algebraic specification languages? 

In theory, there is a clear distinction between languages for model-based specifications, such as VDM and Z, and algebraic languages such as Larch and OBJ. In model-based languages, we describe the operations by defining how they affect models of the values they work on, so a stack may be modelled by a sequence where we add and remove the head to perform push and pop operations. Algebraic languages take the more abstract approach of describing the properties of the operations, so for example we might define the stack by saying that pop(push(x,s)) = s for all stacks s and elements x. There are many ways to model stacks which satisfy this.

In practice, the differences are less marked. Many of the data types that must be defined in an algebraic language (such as sets) are predefined in VDM, and we work with them by using the properties that would be their algebraic specification. When we build models for new data types, we prove that they have the algebraic properties and use them when we exploit those models. Conversely, we cannot usually give a complete axiomatization of a data type by equations alone, and the initial and final approaches to algebraic specification take a particular model as the meaning of the specification. This can then be shown to have the properties that cannot be expressed equationally. Larger specifications are usually built on these basic types in both the algebraic and the model-based styles: definitions in each frequently resemble functional programs.

Subject: How does VDM compare to Z?

The differences between VDM and Z aren't as great as they appear on the page. They are discussed in some detail in the "Magic Roundabout" paper [HJN93].

Subject: What is the relationship between VDM and RSL? 

RSL is the RAISE Specification Language, being developed as part of the RAISE and LaCoS projects. RSL is inspired by VDM and indeed shares a number of syntactic and semantic aspects. However, it adds a property-oriented specification style, modular specification constructs and concurrency. A description of the relationship between the languages can be found in [RAISE92].

Subject: What is the relationship between VDM and the Refinement Calculus? 

To be completed.

Subject: Who is using VDM?

We are starting up a database of information about industrial uses of VDM-SL. If you have information for inclusion, get in touch with Nico Plat, Cap Volmac, Dolderseweg 2, 3712 BP Huis ter Heide, The Netherlands (E-mail: Nico.Plat@ACM.org).

Subject: What sorts of system can VDM be used to describe? 

If you have a look in The VDM Bibliography, you'll see references to the use of VDM in the development of compilers, databases, fault-tolerant storage systems, graphics software, medical warning systems, novel computing architectures, security-critical message processing systems and more. The following book contains 13 case studies in VDM (although it's a fairly advanced text):

C B Jones and R C Shaw (eds) "Case Studies in Systematic Software Development" Prentice-Hall International Series in Computer Science ISBN 0-13-116088-5, 387 pp

There exists a VDM Examples Repository. The repository is maintained by Peter Gorm Larsen (peter@ifad.dk). If you are interested you can either access the examples via ftp or via WWW and Mosaic.

By ftp:

> Site: ftp.ifad.dk (130.225.136.3) Directory: /pub/vdm/examples

By WWW and Mosaic:

http://www.ifad.dk/examples/examples.html

The current set of examples cover the following subjects: "Specification of an ammunition control system", "Railway Interlocking Systems", "Formal Semantics of Data Flow Diagrams", "Specification of the MAA standard", "The Specification of a Binary Relational Database System", "Denotational Semantics of the programming language NewSpeak" and "Looseness Analysis Tool for a VDM-SL Subset".

Subject: What tools are available?

SpecBox is an industrialised tool for inputting, checking and printing VDM specifications. It is composed of four main parts: a syntax checker; a LaTeX generator; a semantic analyser and a translator to the 'Mural' proof assistant. Originally released in 1988, SpecBox is in use in industry in ordnance, avionics, civil nuclear, automotive, railway, security applications and in academic applications. Contact: Peter Froome, Adelard, Coborn House, 3 Coborn Road, London E3 2DA, UK, Tel: +44 (0)81 983 0214, Fax: +44 (0)81 983 1845, Email: pkdf@dcs.ed.ac.uk.

The IFAD VDM-SL Toolbox supports syntax checking, extensive static semantic checking, latex pretty printing, test coverage analysis, execution and source-level debugging. > The toolbox is widely used in industry and research and the > latest release incorporates a C++ code-generator. The toolbox is available from IFAD, Forskerparken 10, 5230 Odense M, DK (tel +45 63 15 71 31, fax +45 65 93 29 99, email peter@ifad.dk).

The Mural system supports formal reasoning about specifications. It can be used to verify the internal consistency of a specification by discharging the appropriate proof obligations. The main component of mural is a proof assistant. Mural also contains a VDM support tool for construction of specifications and refinements. Proof obligations can be generated from these and discharged using the proof assistant. Contact: Dr. Brian Ritchie, Rutherford Appleton Laboratory, Informatics Department, Chilton, Didcot, Oxon OX11 0QX, UK, Tel: +44 (0)235 446147, Fax: +44 (0)235 445831, Email: br@inf.rl.ac.uk.

A free VDM Parser which consists of two variants of a VDM-SL parser. Further information is available from the Technical University of Braunsweig, Institut f\"{u}r Programmiersprachen, Ga\"{u}sstrasse 17, 38092 Braunschweig, Germany. Contact Bernd Fischer (email fisch@ips.cs.tu bs.de), Matthias Kievernagel (email mkiever@ips.cs.tu bs.de) or J\"{o}rg Rhiemeier (email rhiemeir@ips.cs.tu bs.de) for further information.

The Centaur-VDM environment is an interactive and graphical tool for manipulating specifications written in ISO VDM-SL. Besides analyses for syntax and static semantics, it provides help for refinement and the generation of test cases. Contact Phillippe Facon, CEDRIC IIE, Institut d'Informatique d'Entreprise, 18, allee Jean Rostand, F-91025 EVRY CEDEX, France (tel +33 16 1 60 77 97 40 ext. 165, fax +33 16 1 60 77 96 99, email facon@cnam.cnam.fr)

For further information about tools, look in The Formal Methods Tools Database, available by anonymous ftp from chopwell.ncl.ac.uk in directory /pub/fm_tools/, or on World-wide Web at URL ftp://chopwell.ncl.ac.uk/pub/fm_tools/fm_tools_db.

Subject: There's something missing from this FAQ! Whom do I tell? 

The Editor, who is Marcel Verhoef (marcel@dutct05.tudelft.nl).

Originated by John Fitzgerald (vdm-forum-request@mailbase.ac.uk) with contributions from Peter Gorm Larsen, Nico Plat, Cliff Jones, Tim Clement, and other members of the vdm-forum list.

Subject: References

[A+92] M. Andersen, R. Elmstr/om, Poul B/ogh Lassen and Peter Gorm Larsen. Making Specifications Executable -- Using IPTES Meta-IV. Microprocessing and Microprogramming, Vol 35 No 1-5, pp 521-528, September 1992

[BCJ84] H. Barringer, J. H. Cheng and C. B. Jones. A Logic Covering Undefinedness in Program Proofs. Acta Informatica Vol 21, pp 251-269, 1984

[C86] J. H. Cheng. A Logic for Partial Functions, Technical Report, Dept. of Computer Science, University of Manchester, UK, No UMCS-86-7-1, 1986

[CJ91] J. H. Cheng and C. B. Jones. On the usability of logics which handle partial functions. In Proceedings of The 3rd Refinement Workshop, C. Morgan and J. C. P. Woodcock (eds), pp 51-69, Springer-Verlag, 1991

[Cl92] T. Clement. The role of data reification in program refinement. Computer Journal 35(5), pp.451-459, 1992.

[Col94] Pierre Collette. Design of Compositional Proof Systems Based on Assumption-Commitment Specifications -- Application to UNITY. PhD Thesis. Louvain-la-Neuve, 1994

[DvK92] E.H. Durr, J. van Katwijk. VDM++ -- A Formal Specification Language for Object-oriented Designs. In "Computer Systems and Software Engineering", Proceedings of CompEuro'92. IEEE Computer Society press. pages 214-219. 1992.

[DGP94] E.H. Durr, S.J. Goldsack, N. Plat. Rigorous Development of Concurrent and Real-Time Object-oriented Systems. Tutorial presented at TOOLS Europe '94, Versailles, France. 1994.

[DP94] E.H. Durr, N. Plat (editor). VDM++ Language Reference Manual. Afrodite (ESPRIT-III project number 6500) document AFRO/CG/ED/LRM/V9. Cap Volmac, 1994.

[F91] J. S. Fitzgerald. Reasoning about a Modular Model-Oriented Formal Specification. In Harper and Norrie (eds), Proc. Intl. Workshop on Specifications of Database Systems, University of Glasgow 1991. Springer-Verlag Workshops Series. 1992

[F92] N. E. Fuchs. Specifications are (Preferably) Executable. Software Engineering Journal, September 1992, pp323-324

[HJ89] I. J. Hayes and C. B. Jones. Specifications are not (necessarily) executable. Software Engineering Journal Vol 4 No 6, pp 320-338, November 1989

[HJN93] I. J. Hayes, C. B. Jones and J. Nicholls. Understanding the Differences Between VDM and Z. FACS Europe Newsletter, Autumn 1993, pp 7-30. Also available by anonymous ftp as a University of Manchester Technical Report in file pub/TR/UMCS-93-8-1.ps.Z at ftp.cs.man.ac.uk

[JM94] C.B. Jones and C.A. Middelburg. A typed logic of partial functions reconstructed classically. Acta Informatica, 31(5):399--430, 1994

[Jon81] C. B. Jones. Development Methods for Computer Programs including a Notion of Interference. DPhil thesis, Oxford University, printed as Programming Research Group Technical Monograph 25, June, 1981

[Jon83] C. B. Jones. Specification and Design of (Parallel) Programs. Proceedings of IFIP'83, pp 321-332, North-Holland, 1983

[Jon93] C. B. Jones. Reasoning about Interference in an Object-Based Design Method. In FME'93: Industrial-Strength Formal Methods, J. C. P. Woodcock and P. G. Larsen (eds), Springer-Verlag, LNCS series vol 670, pp 1-18, 1993.

[L94] Peter Gorm Larsen. Response to "The Formal Specification of Safety Requirements for Storing Explosives". Formal Aspects of Computing, Vol 6 No 4, 1994

[M93] C. A. Middelburg. Logic and Specification. Chapman and Hall, Computer Science: Research and Practice 1. 1993

[Nip86] T. Nipkow. Nondeterministic data types: models and implementation. Acta Informatica 22, pp.629-661, 1986.

[RAISE92] The RAISE Language Group. The RAISE Specification Language. Prentice Hall BCS Practitioner Series, 1992 ISBN 0-13-752833-7

[Sto90] K. St{\o}len. Development of Parallel Programs on Shared Data-Structures. PhD Thesis 1990, available as Manchester University Tech Report UMCS-91-1-1

[Wills91] Alan C. Wills. Capsules and types in Fresco. ECOOP'91, Springer-Verlag LNCS 512

[Wills92] Alan C. Wills. Specification in Fresco. In Stepney et al, "Object Orientation in Z"(!) Springer-Verlag Workshops Series. 1992

[Wills94] Alan C. Wills. Refinement in Fresco. In Lano & Haughton "OO specification case studies" Prentice Hall Object Orientation Series. 1994

[Xu92] Qiwen Xu. A Theory of State-based Parallel Programming. Phil Thesis, Oxford University, 1992

Home - Vienna - Photos - Music - Traveltips - Tours - Boattrip - Coffeehouse - Heuriger/Wine - Links - Search - About