Modular verification of higher-order methods with mandatory calls specified by model programs

What we call a''higher-order method" (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design pattern...