Hoare logic can be used for proving program correctness (e.g. for deriving correctness statements for the whole program from the statements for the individual commands or constructions; good summary is http://www.cis.upenn.edu/~bcpierce/sf/Hoare.html). The question is - is there any line of research where Hoare-style reasoning can be made for programs that creates and deletes objects.
One thought can be that this reasoning can be simulated by defining large pool of objects which have (for the purposes of correctness analysis) additional state attribute with values from the enumeration {not-created, created, destroyed}. But I guess that better approach should exist.
Are there any references or keywords for furher search into this matter.