A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts