Methods and systems for an interactive theorem-proving tool with reflective capabilities

• US 20040128649A1
• Filed: 12/30/2002
• Published: 07/01/2004
• Est. Priority Date: 12/30/2002
• Status: Active Grant

• Current Assignee: Intel Corporation
• Original Assignee: Intel Corporation
• Inventors: Aagaard, Mark D., Grundy, James D.
• Granted Patent: US 7,181,729 B2
• Time in Patent Office: Days
• US Class Current: 717/106
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

Methods and systems are provided for improved operation of a theorem-proving tool. Logic statements that are to be proved are loaded and a series of interactive commands and assumptions are interactively processed. As the series of commands and assumptions are processed they are tracked. Moreover, the series of commands and assumptions are automatically replayed when a change is received. In some embodiments, the commands are validated for correct syntaxes and data types before the commands are processed.

Claims

1. A method to prove logical statements, comprising:

loading the logic statements;

tracking commands and assumptions inputted by an operator associated with processing and proving the logic statements;

receiving a change that affects the loaded logic statements from the operator after a number of the commands and assumptions have been processed; and

automatically replaying the commands and the assumptions with the change to place the operator in a state after the change was received and processed.

2. The method of claim 1 further comprising validating syntax associated with the commands before processing the commands.

3. The method of claim 1 further comprising, performing type checking on variables and data associated with the commands before processing the commands.

4. The method of claim 1 further comprising, decomposing the logic statements into a plurality of goals and sub goals associated with proving the software module.

5. The method of claim 4 wherein in decomposing, the goals and sub goals are organized as a tree data structure.

6. The method of claim 1 further comprising, making a source associated with the logic statements available to the operator for modifications associated with the change.

7. The method of claim 1 wherein in tracking, the commands and assumptions are used to interactively build executable statements that are processed with the automatic replaying to reach the state by using reflection.

8. An article having a machine accessible medium having associated instructions, wherein the instructions, when executed, result in a theorem-proving tool comprising at least one component performing:

replaying a series of previously processed commands and assumptions associated with logic statements that are being proved after receiving a change during a proofing session; and

resuming the proofing session of the logic statements at a state that represents replaying the series of previously processed commands and assumptions, and processing the change.

9. The article of claim 8 further comprising instructions for presenting a source associated with the logic statements for modification when receiving the change.

10. The article of claim 8 further comprising instructions for decomposing the logic statements into a plurality of goals and sub goals representing sub logic of the logic statements, and wherein the series of previously processed commands and assumptions represent processing a number of the goals or sub goals.

11. The article of claim 8 wherein a number of the assumptions represent assumptions about data that is processed by the logic statements.

12. The article of claim 8 further comprising instructions for validating the series of previously processed commands for acceptable syntax and data types recognized by the logic statements.

13. The article of claim 8 wherein the logic statements are associated with at least one logical model used to determine correct operation of a microprocessor system, a transportation system, a financial system, a medical device, a military system, and a communication system.

14. A theorem-proving system, comprising:

a theorem-proving tool;

logic statements; and

wherein the theorem-proving tool loads the logic statements for interactive processing, and wherein the theorem-proving tool interactively tracks and processes commands and assumptions associated with the logic statements, and wherein the theorem-proving tool automatically replays the commands and assumptions when a subsequent change is received.

15. The theorem-proving system of claim 14 wherein the theorem-proving tool interactively validates syntax, data types, and processing results of the commands.

16. The theorem-proving system of claim 14 wherein the theorem-proving tool makes a source associated with the logic statements available for modification with the subsequent change.

17. The theorem-proving system of claim 14 wherein the theorem-proving tool is implemented in an interpretive and typed software programming language having reflective capabilities.

18. The theorem-proving system of claim 14 wherein the theorem-proving tool constructs a data structure of sub logic statements associated with the logic statements.

19. The theorem-proving system of claim 18 wherein the data structure is represented as a tree with nodes of the tree corresponding to goals and sub goals that represent sub logic statements of the logic statements and that are used to prove the correct operation of the logic statements.

20. The theorem-proving system of claim 14, wherein the commands represent a number of calculations associated with the logic statements and include syntax accepted by the logic statements and data, if necessary, associated with processing the number of the calculations.