The most common way for the software development initialization, is the construction of a program P and a continuous informal referencing to its specifications SP0, which is finally followed by a formal verification of satisfaction among the program and its specifications (SP 0). This verification is done under testing of the calculated input / output of the program in specific selected cases, in conjunction with the satisfaction of the constraints that has been specified in (SP0). Excluding trivial programs, this process has the disadvantage that correctness of the program P cannot be guaranteed, even if the output in all cases of testing is correct. However, there are available methods for automatically generating test cases, which are of subject to expose problems.
In addition, a formal proof of correctness of the program P with respect to its specification SP0 can also be an alternative to testing. To the contrary, with conjecture of many years of work on program verification, this method has been widely accepted as unfeasible for real-life programs. An ideal software system which will have the functionality of automatically generating proofs of program correctness is totally unconsidered.