A method for synthesizing a verification language, and thereby enabling the verification
language to be compiled into a target language. This method enables the underlying
control structure of the verification language to be determined, and then used
to map the dynamic behavior of the verification language onto the target language
as part of a static framework. The process of synthesizing any type of verification
language causes at least a portion of the implicit control structure of the software
program to be constructed into the compiled output code, such that an additional
scheduler or other type of runtime system may not be required. Therefore, the compiled
output code should have a greater execution speed and should be operated more efficiently
than the software programs which are written in the verification language itself.
