SRC Technical Note 2000 003 December 31 2000 Houdini an Annotation Assistant for ESC Java Cormac Flanagan and K Rustan M Leino COMPAQ Systems Research Center 130 Lytton Avenue Palo Alto California 94301 http www research compaq com SRC Copyright Compaq Computer Corporation 2000 All rights reserved Abstract A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program
Houdini an Annotation Assistant for ESC Java Cormac Flanagan and K Rustan M Leino Compaq Systems Research Center 130 Lytton Ave Palo Alto CA 94301 USA cormac flanagan rustan leino compaq com Abstract A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program Modular checking requires that each module be accom panied by annotations that specify the module To help reduce the cost o