Persisted specifications of method pre-and post-conditions for static checking

• US 7,421,680 B2
• Filed: 09/22/2003
• Issued: 09/02/2008
• Est. Priority Date: 09/22/2003
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: DeLine, Robert Anthony, Fahndrich, Manuel Alfred
• Primary Examiner(s): Dam; Tuan Q.
• Assistant Examiner(s): Yigdall; Michael J
• Application Number:
  US10/667,542
• Publication Number:
  US 20050066319A1
• Time in Patent Office: 1,807 Days
• Field of Search: 717/126
• US Class Current: 717/126
• CPC Class Codes: G06F 8/433 Dependency analysis; Data or control flow analysis

Abstract

A system and method employing pre- and/or post-condition(s) specified at a source code level and persisted (e.g., in associated object code and/or a specification repository) facilitating static checking of the object code is provided. The system and method are based, at least in part, upon a framework that employs rules for using an interface to be recorded as declarative specifications in an existing language. The system can employ a range of annotations that allow a developer to specify interface rule(s) with varying precision. At the simplest end of the range, a specifier can mark those methods that allocate and release resource(s). A specifier can also limit the order in which an object'"'"'s methods may be called to the transitions of a finite state machine. At the more complex end of the range, a specifier can give a method a plug-in pre- and post condition, which is arbitrary code that examines an object'"'"'s current state and a static approximation of the method'"'"'s actuals, decides whether the call is legal and returns the object'"'"'s state after the call.

Claims

1. An executable code check computing system comprising:

an input component operating on computer hardware that receives an executable object file having an embedded specification that is removable, the specification specified at a source code level by embedding the specification within source code of the executable object file; and

a checker operating on computer hardware that employs the specification to facilitate static checking of the executable object file, the checker providing information if a fault condition is determined, the fault condition is based on one or more of a violation of rules for using an interface, system resource management rules, rules for proper ordering of method calls, or string parameter format rules.

2. The system of claim 1, the checker further removing the embedded specification from the object file.

3. The system of claim 1, the specification comprising information associated with a method that performs at least one of allocation and release of a resource.

4. The system of claim 1, the specification comprising information associated with an order in which methods of an object can be called.

5. The system of claim 4, wherein method order is constrained by specifying a finite state machine in which the states have symbolic names and transitions between states are labeled with method names.

6. The system of claim 1, the specification comprising a state-machine protocol wherein a method specifies a pre-state and a post-state.

7. The system of claim 1, the specification comprising information associated with a transition of a finite state machine.

8. The system of claim 1, the specification comprising information associated with a state-machine protocol.

9. The system of claim 1, the specification comprising an attribute associated with at least one of a field and a parameter providing information associated with whether or not the at least one of a field and a parameter can be aliased.

10. The system of claim 1, wherein the specification facilitates modeling of a heap modeling.

11. The system of claim 10, the checker employing an algorithm that performs a data flow analysis over the heap model comprising a typing environment and a set of capabilities.

12. An executable code check computing system comprising:

an input component operating on computer hardware that receives an object file;

a checker operating on computer hardware that employs a removable specification embedded in the object file to facilitate static checking of the object file, the checker providing information if a fault condition is determined, the specification specified at a source code level by embedding the removable specification within source code of the object file, the removable specification is removed and stored in a specification repository.

13. The system of claim 12, further comprising the specification repository.

14. A method of facilitating static checking of executable code comprising:

receiving executable code with an embedded specification that is removable, the specification specified at a source code level by embedding the specification within source code of the executable code;

statically applying the specification to the executable code;

determining whether a fault condition exists based, at least in part, upon the statically applied specification; and

providing information associated with the fault condition, if a fault condition is determined to exist.

15. The method of claim 14, further comprising removing the embedded specification from the executable code.

16. A computer readable medium having stored thereon computer executable instructions for carrying out the method of claim 14.