Automatic program synthesis using monadic second-order logic
AssigneeInternational Business Machines Corporation
InventorTakaaki Tateishi
Life of this patent
Estimating the term…
Abstract
A method is provided for synthesizing a computer program by a hardware processor and a program synthesizer. The method includes representing program components and registers by position set variables and constraints on the position set variables using Monadic Second-Order Logic. The method further includes determining potential combinations of the program components by solving the constraints. The method also includes forming the computer program from at least one of the potential combinations.
Claims19
A method for synthesizing a computer program by a hardware processor and a program synthesizer, the method comprising:
- representing program components and registers by position set variables and constraints on the position set variables using Monadic Second-Order Logic, the constraints comprising one or more register syntax constraints;
- determining potential combinations of the program components by solving the constraints;
- and
- forming the computer program by automatically synthesizing the computer program from at least one of the potential combinations, the automatically synthesizing being performed using the program synthesizer executing on the hardware processor.
A computer program product for synthesizing a computer program by a hardware processor and a program synthesizer, the computer program product comprising a non-transitory computer readable storage medium having program instructions embodied therewith, the program instructions executable by a computer to cause the computer to perform a method comprising:
- representing program components and registers by position set variables and constraints on the position set variables using Monadic Second-Order Logic, the constraints comprising one or more register syntax constraints;
- determining potential combinations of the program components by solving the constraints;
- and
- forming the computer program by automatically synthesizing the computer program from at least one of the potential combinations, the automatically synthesizing being performed using the program synthesizer executing on the hardware processor.
Dependencies are inferred from the claim text.