Matthew Smith and Sophia Drossopoulou
Cheaper reasoning with ownership types
In ECOOP 2003 International Workshop on Aliasing and
Confinement, 2003
We use ownership types to facilitate program
verification. Namely, an assertion that has been
established for a part of the heap which is
unaffected by some execution will still hold after
this execution. We use ownership and effects, and
extend them to assertions to be able to make the
judgement as to which executions do not affect which
assertions. We describe the ideas in terms of an
example, and outline the formal system.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43