Frank S. de Boer

What can be proved about an object-oriented program, and at what cost: a WP-calculus and syntax-directed Hoare logic for OO, then the completeness question that runs through the textbook on sequential and concurrent programs and on to reasoning about call-by-value. The second half asks the same question of code somebody actually runs -- the OpenJDK sorting defect found by proving the specification could not hold, and the LinkedList, abstract-data-type and history-based work that follows from it. A third strand approaches the same programs through what a component may touch, in footprint and dynamic separation logic.