Résumé:
The LOOP project focuses on the verification of Java programs annotated with
JML specifications. For this purpose, the LOOP project has developed the LOOP
tool that automatically translates these programs with their specifications
into PVS. This talk briefly explains how this translation works.
The talk elaborates on the semantics used to verify that the Java
implementations satisfy their specifications. A Hoare-like correctness
statement, similar to a Hoare triple {P} S {Q}, is used to cover all the
possible termination modes in Java, including the throwing of exceptions.
They are generated by the LOOP tool and give rise to the desired proof
obligations. Some technical details about the semantics of JML will arise
here.
Retour au sommaire / Back to schedule