Reasoning About Frame Properties In Object-Oriented Programs