Methods and apparatus for generating a verified algorithm for transforming a program from a first form to a second form

• US 6,343,372 B1
• Filed: 06/11/1999
• Issued: 01/29/2002
• Est. Priority Date: 06/11/1999
• Status: Expired due to Term

• Current Assignee: WSOU Investments, LLC (WSOU Holdings, LLC)
• Original Assignee: Lucent Technologies, Inc. (Nokia Corporation)
• Inventors: Felty, Amy Patricia, Roychoudhury, Abhik, Howe, Douglas J.
• Primary Examiner(s): DAM, TUAN QUANG
• Application Number:
  US09/330,526
• Time in Patent Office: 963 Days
• Field of Search: 717/1, 717/2, 717/4, 717/7, 717/8, 706/59, 706/45, 706/922, 703/2
• US Class Current: 717/136
• CPC Class Codes: G06F 8/30 Creation or generation of source code
• CPC Class Codes: G06F 8/40 Transformation of program code

Abstract

A method of synthesizing an algorithm for transforming a program from a first form to a second form includes first formalizing a language associated with the program to be transformed in accordance with a theorem proving system. Then, a proof is built in accordance with the theorem proving system based on a theorem asserting a representability associated with the program, the representability being expressed as inductive predicates over semantic domains. The method then extracts the algorithm based on the proof. The algorithm is capable of transforming the program from the first form to the second form. In one embodiment, the algorithm is a correctness verified abstraction algorithm and the theorem proving system is Nuprl.

Claims

1. A method of synthesizing an algorithm for transforming a program from a first form to a second form, the method comprising the steps of:

formalizing a language associated with the program to be transformed in accordance with a theorem proving system;

building a proof in accordance with the theorem proving system based on a theorem asserting a representability associated with the program, the representability being expressed as inductive predicates over semantic domains; and

extracting the algorithm based on the proof such that the algorithm is capable of transforming the program from the first form to the second form.

2. The method of claim 1, wherein the synthesized algorithm is an abstraction algorithm such that the first form of the program is concrete and the second form of the program is abstracted.

3. The method of claim 2, wherein the synthesized abstraction algorithm is correctness verified with respect to the program applied thereto for transformation.

4. The method of claim 1, wherein the proof reasons on semantics associated with the program language while the extracted algorithm is capable of operating on syntax associated with the program language.

5. The method of claim 1, wherein the theorem proving system is Nuprl.

6. The method of claim 1, wherein the building step implements a possibility operator which expresses representability when the extracted algorithm is a partial function.

7. The method of claim 1, wherein representability is parameterized.

8. The method of claim 1, wherein representability implements one or more variants of standard logic connectives.

9. Apparatus for synthesizing an algorithm for transforming a program from a first form to a second form, the apparatus comprising:

at least one processor operative to formalize a language associated with the program to be transformed in accordance with a theorem proving system, to build a proof in accordance with the theorem proving system based on a theorem asserting a representability associated with the program, the representability being expressed as inductive predicates over semantic domains, and to extract the algorithm based on the proof such that the algorithm is capable of transforming the program from the first form to the second form; and

memory, coupled to the at least one processor, for storing at least a portion of results associated with formalizing, building, and extracting operations.

10. The apparatus of claim 9, wherein the synthesized algorithm is an abstraction algorithm such that the first form of the program is concrete and the second form of the program is abstracted.

11. The apparatus of claim 10, wherein the synthesized abstraction algorithm is correctness verified with respect to the program applied thereto for transformation.

12. The apparatus of claim 9, wherein the proof reasons on semantics associated with the program language while the extracted algorithm is capable of operating on syntax associated with the program language.

13. The apparatus of claim 9, wherein the theorem proving system is Nuprl.

14. The apparatus of claim 9, wherein the building operation implements a possibility operator which expresses representability when the extracted algorithm is a partial function.

15. The apparatus of claim 9, wherein representability is parameterized.

16. The apparatus of claim 9, wherein representability implements one or more variants of standard logic connectives.

17. An article of manufacture for synthesizing an algorithm for transforming a protocol from a first form to a second form, comprising a machine readable medium containing one or more programs which when executed implement the steps of:

formalizing a language associated with the program to be transformed in accordance with a theorem proving system;

building a proof in accordance with the theorem proving system based on a theorem asserting a representability associated with the program, the representability being expressed as inductive predicates over semantic domains; and

extracting the algorithm based on the proof such that the algorithm is capable of transforming the program from the first form to the second form.