 |
| |
|
[ people ] |
|
|
@ Bernhard Reus (PI)
@ Jan Schwinghammer (PhD student now in Saarbrücken)
|
| |
|
[ summary ] |
|
The aim of this project is to develop semantic models of objects that have enough properties to support a programming logic and to set up such a logic on denotations of objects in order to investigate its strengths and limitations. It is expected that the recursive character of objects and their specifications is much better understood on the denotational level.
The project goals will be achieved by defining a realizability semantics of Abadi and Cardelli's functional object calculus in a direct style. By establishing proof principles for objects in the model one obtains a basic programming logic. These proof principles will be based on fixpoint induction or coinduction. It is investigated which interesting properties of object-based programs can be formulated and proved in this logic. Then the same procedure is to be repeated for a typed and an imperative version of the object calculus. The resulting logic shall then be used to verify a syntactic (Hoare-like) calculus for program verification in a direct style by using the denotational semantics of the language instead of the more syntactical operational semantics.
Finally, if time permits, the results shall be transferred to class-based languages like Featherweight Java and ideally protoypically implemented by means of a theorem prover.
|
| |
|
[ Publications ] |
|
B. Reus.
Class based vs.~object based: A denotational comparison. In Algebraic Methodology And Software Technology, volume 2422
of Lecture Notes in Computer Science, pages 473--488, Berlin, 2002.
Springer.
B. Reus.
Modular semantics and logics of classes.
In Computer Science Logic, volume 2803 ofLecture Notes in
Computer Science, pages 456--469, Berlin, 2003. Springer.
B. Reus and J. Schwinghammer.
Denotational semantics for Abadi and Leino's logic of objects. Technical Report 03/04, University of Sussex, 2004.
B. Reus and J. Schwinghammer.
Denotational semantics for Abadi and Leino's logic of objects.
In Mooly Sagiv, editor, European Symposium on Programming,
volume 3444 of Lecture Notes in Computer Science, pages 263--278,
Berlin, 2005. Springer.
B. Reus and J. Schwinghammer.
Denotational semantics for Abadi and Leino's logic of objects.
submitted to MSCS.
B. Reus and Th. Streicher.
Semantics and logics of objects.
In Proceedings of the 17th Symp. Logic in Computer Science,
pages 113--122, 2002.
B. Reus and Th. Streicher.
Semantics and logic of object calculi. TCS, 316:191--213, 2004.
B. Reus and Th. Streicher. About Hoare Logics for Higher-order Store.
In Luis Caires et al., editors, Proceedings of the 32th Intern.
Conference on Automata, Languages, and Programming}, volume 3580 of
LNCS, pages 1337--1348, 2005.
J. Schwinghammer.
A typed semantics for languages with higher-order store and
subtyping.
Technical Report 05/05, University of Sussex, 2005.
J. Schwinghammer.
A typed semantics of higher-order store and subtyping.
In ICTCS'05, 2005. To appear.
|
| |
|
[ further documents ] |
|
[ Royal Society | British Council | ARC |
EPSRC | Uni Grant Office ]
|
|
