Methods and systems for automatically generating provably correct computer program code

• US 20050137992A1
• Filed: 12/19/2003
• Published: 06/23/2005
• Est. Priority Date: 12/19/2003
• Status: Active Grant

• Current Assignee: Goss International Americas Incorporated (City of Shanghai)
• Original Assignee: Fuji Xerox Company Limited (Xerox Holdings Corp.)
• Inventors: Polak, Wolfgang H.
• Granted Patent: US 7,243,086 B2
• Time in Patent Office: Days
• US Class Current: 706/13
• CPC Class Codes: G06F 8/30 Creation or generation of source code
• CPC Class Codes: G06N 3/126 Evolutionary algorithms, e.g. genetic algorithms or genetic programming

Abstract

A provably correct computer program can be 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 technique. A fitness function is applied to measure a distance between the meaning of a 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, 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.

Claims

1. A method of generating a computer program using genetic programming techniques, comprising:

providing a specification which defines the desired program behavior;

creating a current population of programs, each program having an actual behavior;

computing, for each program in the current population, a fitness for that program using a fitness function that computes how well that program satisfies the specification.

2. The method of claim 1, wherein computing the fitness for each program comprises determining a measure of a distance between that program'"'"'s actual behavior and the specification.

3. The method of claim 2, further determining that a program satisfies the specification when the fitness function returns a distance that is within an acceptable tolerance.

4. The method of claim 2, further determining that a program satisfies the specification when the fitness function returns a distance of zero.

5. The method of claim 1, further comprising creating a new population of programs by performing at least one of a mutation operation and a crossover operation on at least one selected program in the population of programs when all programs in the population have been analyzed for fitness without sufficiently satisfying the specification.

6. The method of claim 1, further comprising formalizing the actual behavior of each program being analyzed using denotational semantics techniques.

7. A system that generates programming code using genetic programming techniques, comprising:

a specification receiving circuit, routine or application that receives a specification defining at least one desired program behavior;

a current program population generating circuit, routine or application that generates a population of computer programs, each program having an actual behavior;

a fitness determining circuit, routine or application that determines a fitness of a program in satisfying the specification based on the received specification and a defined fitness function.

8. The system of claim 7, wherein the fitness determining circuit, routine or application applies the fitness function to a program to determine a measure of a distance between that program'"'"'s actual behavior and the specification.

9. The system of claim 8, wherein the fitness determining circuit, routine or application determines that a program satisfies the specification when that program has a distance value within an acceptable tolerance.

10. The system of claim 8, wherein the fitness determining circuit, routine or application determines that a program satisfies the specification when that program has a distance value of zero.

11. The system of claim 7, further comprising a new population generating circuit, routine or application that creates a new population of programs by applying at least one of a mutation operation and a crossover operation on at least one selected program of the current population of programs when all programs in the current population have been analyzed for fitness without any programs sufficiently satisfying the specification.

12. The system of claim 7, wherein the fitness determining circuit, routine or application uses denotational semantics techniques to formalize the actual behavior of each program.

13. The system of claim 8, wherein the fitness determining circuit, routine or application uses test cases to determine fitness of programs by determining if the program can satisfy one or more test cases.

14. A storage medium storing a set of program instructions executable on a data processing device and usable to generate a computer program using genetic programming techniques, comprising:

instructions for receiving a specification of the desired program behavior;

instructions for creating a current population of computer programs, each program having a meaning; and

instructions for applying a fitness function to analyze a fitness of a program in satisfying the specification.

15. The storage medium according to claim 14, wherein the instructions for applying a fitness function to analyze a fitness of the program comprise instructions for applying the fitness function to determine a measure of a distance value between the program'"'"'s actual behavior and the specification.

16. The computer-readable storage medium according to claim 15, further comprising instructions for determining that a program satisfies the specification when the distance value of the fitness function is within an acceptable tolerance.

17. The computer-readable storage medium according to claim 15, further comprising instructions for determining that a program satisfies the specification when the distance value of the fitness function is zero.

18. The computer-readable storage medium according to claim 14, further comprising instructions for creating a new population of programs by performing at least one of a mutation operation and a crossover operation on at least one individual in the current population of programs when all programs in the current population have been analyzed for fitness without any programs sufficiently satisfying the specification.

19. The computer-readable storage medium according to claim 14, further comprising instructions that apply denotational semantics techniques to formalize the actual behavior of that program.