This work was supported in part by NSF grants CCR-9503168 and CCR-9803843. Thanks to Adrian Fiech and Rustan Leino for suggestions and comments on earlier drafts. Rustan's comments led to several improvements in the semantics. Thanks also to Yoonsik Cheon, who helped design Larch/C++, and to Matt Markland who helped implement the Larch/C++ checker.