Verifying Java Programs By Theorem Prover HOL

Program verification plays an important role in assuring the reliability of software systems. This paper presents a novel verification methodology for Java programs based on the higher-order logic theorem proving system HOL. The soundness of a Java program in accordance with its specification in annotation is established in HOL4. A Hoare-logic based verification methodology (WHY) guides the verification process. As a case study, a Java program with four methods is specified in JML annotation and proved in HOL. The flexible manipulation of pure method call in annotation is presented in the HOL proof mechanism. This work may constitute the first attempt on using the proving system HOL for Java programs. The experience demonstrates the effectiveness and the promising results of the approach