Formality based genetic programming

Genetic programming (GP) is an illogical method for automatic programming. It shows creativity in discovering a desired program to solve problem, but in essence bases its searching principle on software testing. This paper is dedicated to establishing a novel GP which combines classical GP and formal approaches like Hoarepsilas logic, model checking, and automaton, etc. The result indicates these methods can collaborate in the framework pretty well. As has been demonstrated by the experiment, they work in a way that preserves their advantages while each compensates for the deficiencies of the other. So, once an approximate program is obtained, we can say with certainty it is correct with respect to its corresponding pre- and post-conditions.