A Method to Generate Verification Condition Generator

We propose a method to generate certain verification condition generators (VCGens, for short) automatically to be used in certifying compilers or other verification tools in this paper, to alleviate the burden of developing various kinds of VCGens in the domain-specific program verification tools. We introduce a new methodology for describing the rules in the verification condition calculation. We have implemented a prototype of VCGEN2(VCGenGen) using C++. This tool provides a series of interfaces named action functions to the users. Users can describe the calculation rules by combining these action functions. And our tool also embeds a parser generator, so users need to feed in the grammar of the languages along with the calculation rules. If there is no error, VCGEN2 outputs the corresponding VCGen with respect to the user-defined languages and rules. We have used our prototype to generate a number of VCGens successfully as demonstration.