Method and apparatus for automatically inferring annotations for an extended static checker

摘要

A system, method and computer program product for annotating a computer program. The method includes inserting a set of heuristically derived candidate annotations into the computer program and converting the computer program into a verification condition-which includes a set of guards corresponding to the set of candidate annotations. Initial truth values are assigned to the guards. A theorem prover is applied to the verification condition, and the counter-examples are mapped into one or more annotation modifications. The truth value of at least one of the guards corresponding to the one or more annotation modifications is updated. The theorem proving, mapping and truth value updating steps are repeated until the theorem prover produces no counter-examples that are suitable for mapping into an annotation modification. The resulting annotation modifications are applied to the computer program. The system and computer program product implement this method of annotating a computer program.