rhys@batserver.cs.uq.oz.au (Rhys Weatherley) (06/02/90)
Here is a summary of the responses I got for my formal verifications request in comp.lang.eiffel a little while ago plus a few other "useful things": 1. MIT PhD thesis by Gary Leavens: leavens@bambam.cs.iastate.edu Gary T. Leavens. Verifying object-oriented programs that use subtypes. Technical Report 439, MIT, Laboratory for Computer Science, February 1989. 2. Object-Z: Contact Roger Duke: rduke@batserver.cs.uq.oz.au This is a development by the University of Queensland's Computer Science Department. It is a set of extensions to the Z specification language to allow for specifications of object-oriented programs and systems. The main paper at present is: D.Carrington, D.Duke, R.Duke, P.King, G.Rose and G.Smith. Object-Z: An object-oriented extension to Z. In Formal Description Techniques (FORTE'89). North Holland, 1990. So far, work with Object-Z has mainly been from a specification rather than verification standpoint, but Roger Duke at the e-mail address above can tell you more about it. 3. Pierre America and Frank de Boer, now at the Eindhoven University of Technology, have developed formal proof systems for two object-oriented languages, a sequential and a parallel one. They use a kind of Hoare logic, where the language in which the assertions are written has been specially devised to deal with arbitrary pointer structures. Both systems have been proved to be sound and complete. Publications are on their way, but anyone who is interested can get the reports; just send your (ordinary mail) address to: Pierre America Philips Research Laboratories P.O. Box 80.000 5600 JA Eindhoven The Netherlands america@prles6.prl.philips.nl Note: I have contacted Pierre, but haven't received any replies yet. ------- My honours project itself will not be available till the end of the year, but I will endeavour to see that everyone who wants a copy gets one. It is being modelled within "Functional Logic" and "Functional Set Theory", which are local developments here at the University of Queensland. My aim is to add extra definitions and theories to deal with object-oriented concepts. Two of the introductory Technical Reports dealing with these subjects are shown below: J.Staples, P.Robinson and D.Hazel, A Functional Logic for Higher Level Reasoning About Computation. Tech. Rept No. 141, Key Centre for Software Technology, Dept. of Comp. Sci., University of Queensland, December 1989. P.Henman and J.Staples, Introduction to Functional Set Theory, Tech. Rept No. 144, Key Centre for Software Technology, Dept. of Comp. Sci., University of Queensland, February 1990. To find out more about these topics, contact John Staples: staples@uqcspe.cs.uq.oz.au If anyone has anything to add to the list above, pertaining to verification of object-oriented programs, then contact me at the e-mail address below and I will maintain a summary and post it regularly if there is a lot of demand. Rhys. +===============================+==============================+ || Rhys Weatherley | University of Queensland, || || rhys@batserver.cs.uq.oz.au | Australia. G'day!! || +===============================+==============================+