Formal verificatinon methods for OOPS 
Author Message
 Formal verificatinon methods for OOPS

I am currently doing an honours project in modelling Object-Oriented Concepts
for the purposes of verification of programs written in Object-Oriented
languages.

I am interested if any work in this field has already been done, especially
as it pertains to Eiffel.  Although I'm not explicitly using Eiffel for
the target language, I am attempting to model many of the features that
Eiffel embodies.

By verification here, I mean showing that the bodies of procedures and
functions, etc that act on objects do in fact satisfy the assertions
about objects of a particular class.  One method would be to use
'Hoare Logic' ({Pre-condition} CODE {Post-condition} triples) as has
been applied to Pascal programs (and probably others as well).  Both
hand and automatic verification techniques are acceptable.

Thanks in advance for any replies this request may generate.

Rhys.

+===============================+==============================+
||  Rhys Weatherley             |  University of Queensland,  ||

+===============================+==============================+



Sat, 31 Oct 1992 14:39:33 GMT  
 Formal verificatinon methods for OOPS

Quote:

>I am currently doing an honours project in modelling Object-Oriented Concepts
>for the purposes of verification of programs written in Object-Oriented
>languages.

Together with Frank de Boer, now at the Eindhoven University of Technology, I
have developed formal proof systems for two object-oriented languages, a
sequential and a parallel one. We 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 me.

Pierre America
Philips Research Laboratories
P.O. Box 80.000
5600 JA Eindhoven
The Netherlands



Mon, 02 Nov 1992 21:45:58 GMT  
 Formal verificatinon methods for OOPS
Sorry to post this here, when try to reply to the original article
my mail bounced.

In comp.object you write:

Quote:
>Together with Frank de Boer, now at the Eindhoven University of Technology, I
>have developed formal proof systems for two object-oriented languages, a
>sequential and a parallel one. We 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 me.

Could you please send me one, my mail address is:

Dept Computer Science,
University of Qld,
St Lucia,
Qld 4072,
Australia

Also if your computer has access to ftp, why don't you make it available
for ftp ?



--
Anthony Lee (Humble PhD student) (Alias Time Lord Doctor)


SNAIL: Dept Comp. Science, University of Qld, St Lucia, Qld 4072, Australia



Fri, 06 Nov 1992 17:43:34 GMT  
 
 [ 4 post ] 

 Relevant Pages 

1. Formal verification methods for OOPS

2. Formal methods for verification of OOPS

3. Formal methods and Eiffel

4. "Formal" testing methods in Forth

5. CfP: 2nd IRISH WORKSHOP ON FORMAL METHODS

6. Announcing: Formal Methods in Computer Science Workshop

7. FACS Europe --- A Formal Methods Newsletter

8. Open positions in Formal Methods and their Applications

9. Announcing: Formal Methods in Computer Science Workshop

10. GSL collaboration and formal methods.

11. Formal methods research sources wanted

12. IDPT 2002 Session: Formal Methods in Healthcare [2nd call for paper]

 

 
Powered by phpBB® Forum Software