Can Hoare logic be used when objects are created or deleted? 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.
There is a lot of work on Hoare Logic for object oriented programs, and for reasoning about memory allocation and deallocation. Some starting points:


A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts
Separation Logic, does not target OO-languages specifically but applies to the more fundamental problem of reasoning about heap-allocated data.
jStar: Bringing separation logic to Java