[Acpc-l] Talk by Bertrand Meyer - 14.3.03 TU Wien
Renate Weiss
weiss@infosys.tuwien.ac.at
Tue, 04 Mar 2003 14:45:22 +0100
--=====================_16971313==_.ALT
Content-Type: text/plain; charset="iso-8859-1"; format=flowed
Content-Transfer-Encoding: quoted-printable
Einladung zum Vortrag
Towards practical correctness proofs of object-oriented software
Bertrand Meyer, ETH Z=FCrich / Eiffel Software
Friday, 14 March 2003, 16.30 h
FH HS 2 (Turm B, 2. Obergescho=DF, gelber Bereich)
Wiedner Hauptstra=DFe 8-10, 1040 Wien
Abstract
--------
In the search for "Trusted Components" -- reusable software elements with
guaranteed quality properties -- one of the ultimate goals is to equip some
components with full correctness proofs. A first target for this effort
is provided by object-oriented libraries, whose components, although
relatively fine-grain, play a major role in everyday software development.
I will present a general approach for proving that contract-equipped
classes such as those of the EiffelBase library satisfy their contracts.
The method uses a mix of denotational and axiomatic techniques, focusing
at first on the notion of object (rather than class) and including a
comprehensive model of the run-time structure and especially
the presence of pointers, for which I will describe a new mathematical
model taking advantage of the power of functions and relations. The
approach is object-oriented to the core, giving the notion of "current
object" a central role and respecting the rules of information hiding.
The results obtained so far yield a simple semantics of object-oriented
computation and make it possible to prove non-trivial class operations
such as insertion, deletion and reversal in a LINKED_LIST class.
Speaker
-------
Bertrand Meyer is professor of software engineering at ETH Z=FCrich,
founder of Eiffel Software, and author of several books including
"Object-Oriented Software Construction".
Home page at ETH: http://www.inf.ethz.ch/personal/meyer/
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
Renate Weiss
Sekretariat Prof. Mehdi Jazayeri
Technische Universit=E4t Wien / Institut f=FCr Informationssysteme
Argentinierstrasse 8/184-1, A-1040 Wien
Tel: +43-1-58801-18402 FAX: +43-1-58801-18491
Email: weiss@infosys.tuwien.ac.at
URL: http://www.infosys.tuwien.ac.at=20
--=====================_16971313==_.ALT
Content-Type: text/html; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
<html>
<br>
Einladung zum Vortrag<br><br>
<b>Towards practical correctness proofs of object-oriented software<br>
</b>Bertrand Meyer, ETH Z=FCrich / Eiffel Software<br><br>
<b>Friday, 14 March 2003, 16.30 h<br>
</b>FH HS 2 (Turm B, 2. Obergescho=DF, gelber Bereich)<br>
Wiedner Hauptstra=DFe 8-10, 1040 Wien<br><br>
<br>
Abstract <br>
--------<br>
In the search for "Trusted Components" -- reusable software
elements with <br>
guaranteed quality properties -- one of the ultimate goals is to equip
some <br>
components with full correctness proofs. A first target for this effort
<br>
is provided by object-oriented libraries, whose components, although
<br>
relatively fine-grain, play a major role in everyday software
development. <br>
I will present a general approach for proving that contract-equipped
<br>
classes such as those of the EiffelBase library satisfy their contracts.
<br>
The method uses a mix of denotational and axiomatic techniques, focusing
<br>
at first on the notion of object (rather than class) and including a
<br>
comprehensive model of the run-time structure and especially <br>
the presence of pointers, for which I will describe a new mathematical
<br>
model taking advantage of the power of functions and relations. The=20
<br>
approach is object-oriented to the core, giving the notion of
"current <br>
object" a central role and respecting the rules of information
hiding.<br>
The results obtained so far yield a simple semantics of object-oriented
<br>
computation and make it possible to prove non-trivial class operations
<br>
such as insertion, deletion and reversal in a LINKED_LIST class.<br>
Speaker <br>
------- <br>
Bertrand Meyer is professor of software engineering at ETH Z=FCrich, <br>
founder of Eiffel Software, and author of several books including <br>
"Object-Oriented Software Construction".<br>
Home page at ETH:
<a href=3D"http://www.inf.ethz.ch/personal/meyer/" eudora=3D"autourl"><font=
color=3D"#0000FF"><u>http://www.inf.ethz.ch/personal/meyer/</a><br><br>
</u></font>=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D<br>
Renate Weiss <br>
Sekretariat Prof. Mehdi Jazayeri <br>
Technische Universit=E4t Wien / Institut f=FCr Informationssysteme <br>
Argentinierstrasse 8/184-1, A-1040 Wien <br>
Tel: +43-1-58801-18402 FAX: +43-1-58801-18491 <br>
Email: weiss@infosys.tuwien.ac.at <br>
URL:
<a href=3D"http://www.infosys.tuwien.ac.at/" eudora=3D"autourl"><font color=
=3D"#0000FF"><u>http://www.infosys.tuwien.ac.at</a></u></font>
</html>
--=====================_16971313==_.ALT--