Cristiano Calcagno
Program logics in the presence of Garbage Collection
Garbage collection relieves the programmer of the burden of
managing dynamically allocated memory, by providing an automatic way
to reclaim unneeded storage. This eliminates or lessens program
errors that arise from attempts to access disposed memory, and
generally leads to simpler programs. One might therefore expect that
reasoning about programs in garbage collected languages would be much
easier than in languages where the programmer has more explicit
control over memory. But existing program logics are based on a low
level view of storage that is sensitive to the presence or absence of
unreachable cells, and Reynolds has pointed out that the Hoare triples
derivable in these logics are even incompatible with garbage
collection. We present a semantics of program logic assertions based
on a view of the heap as finite, but extensible; this is for a logical
language with primitives for dereferencing pointer expressions. The
essential property of the semantics is that all propositions are
invariant under operations of adding or removing garbage cells; in
short, they are garbage insensitive. We use the assertion language to
formulate notions of partial and total correctness for a small
programming language, and provide logical characterizations of two
natural notions of observational equivalence between programs.
Host: John Reynolds
POP Seminar
February 23, 2001
3:30 p.m.
Wean Hall 8220