METHOD AND SYSTEM FOR AUTOMATICALLY GENERATING PROVABLY CORRECT COMPUTER PROGRAM CODE

摘要

PPROBLEM TO BE SOLVED: To provide a method and system for evolving a program to the program suitable for specifications, namely, the provably correct program using formal specifications and evolutional algorithm in which desired behaviors of the program is defined. PSOLUTION: This provably correct computer program is generated using genetic programming techniques. A desired behavior is used to define a formal specification. An initial population of programs is created where each program has a meaning that can be defined using a formalization techniques. A fitness function is applied to measure a distance between the meaning of the program, i.e., its actual behavior, and the specification. Any program having a zero value as the measure of distance between the meaning of the program and the specification is determined to be provably correct. After the fitness of some or all of the programs in the current generation of programs has been computed, when a provably correct program has not yet been found in the current generation, mutation and/or crossover techniques are performed on at least some of the fittest individuals in the current generation to create the programs of a next generation. PCOPYRIGHT: (C)2005,JPO&NCIPI