Persisted specifications of method pre-and post-conditions for static checking
View Patent ↗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.
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 .