Methods and systems for automatically generating provably correct computer program code
First Claim
1. A computer implemented method of generating a computer program using genetic programming techniques, comprising:
- providing a specification which defines a desired program behavior;
creating a current population of programs, each program having an actual behavior;
providing a mapping that maps each program in the current population onto the specification of the desired program behavior without the need for executing the program;
computing, for each program in the current population, a fitness for that program using a fitness function that computes the difference between the mapping of the program and the specification of the desired program behavior; and
,when an acceptable computed fitness has been calculated for one of the programs, outputting that program as a provable correct program.
3 Assignments
0 Petitions
Accused Products
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.
11 Citations
19 Claims
-
1. A computer implemented method of generating a computer program using genetic programming techniques, comprising:
-
providing a specification which defines a desired program behavior; creating a current population of programs, each program having an actual behavior; providing a mapping that maps each program in the current population onto the specification of the desired program behavior without the need for executing the program; computing, for each program in the current population, a fitness for that program using a fitness function that computes the difference between the mapping of the program and the specification of the desired program behavior; and
,when an acceptable computed fitness has been calculated for one of the programs, outputting that program as a provable correct program. - View Dependent Claims (2, 3, 4, 5, 6, 7)
-
-
8. A computerized 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 program analyzing circuit, routine or application that maps each program in the current population onto the specification without executing the program; a fitness determining circuit, routine or application that determines a fitness of a program in satisfying the specification based on the mapping onto the received specification and a defined fitness function, and when an acceptable computed fitness has been determined for one of the programs, outputs that program as a provable correct program. - View Dependent Claims (9, 10, 11, 12, 13)
-
-
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; instructions for mapping each of said programs onto said specification without executing the program; and instructions for applying a fitness function to analyze a fitness of the mapping of a program in satisfying the specification and when an acceptable computed fitness has been calculated for one of the programs, outputting that program as a provable correct program. - View Dependent Claims (15, 16, 17, 18, 19)
-
Specification