Patent ID: 8584093
Filing Date: 2013-11-12
Classification: G06F

Abstract:
1. A computer-implemented pre-condition generation method, comprising: accessing a program storage configured to store a program described by an imperative programming language; accessing a post-condition storage configured to store a post-condition of the program, the post-condition being a logical product of one or more first logical expressions; accessing a logical expression storage configured to store a plurality of second logical expressions; accessing an essential condition storage configured to store an essential condition which is a set of one or more second logical expressions selected from the logical expression storage such that a proposition is not satisfied that the post-condition is satisfied immediately after execution of the program when a logical product of other second logical expressions obtained by excluding the essential condition from all second logical expressions in the logical expression storage is satisfied before execution of the program; generating a candidate condition being a logical product of one or more second logical expressions selected from the logical expression storage so as to include at least one common second logical expression with the essential condition; judging whether there is a counterexample to a proposition that the post-condition is satisfied immediately after execution of the program when the candidate condition is satisfied before execution of the program, and determining that the proposition is satisfied when the counterexample is not existent and that the proposition is not satisfied when the counterexample is existent; and outputting the candidate condition satisfying the proposition as a pre-condition of the program.