Persisted specifications of method pre-and post-conditions for static checking
US7421680B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Sep 22, 2003 |
| Grant date | Sep 2, 2008 |
| Priority date | — |
| Expiry date | Oct 14, 2025 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F8/433
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.