Plug-in pre- and postconditions for static program analysis
US7526755B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Oct 8, 2003 |
| Grant date | Apr 28, 2009 |
| Priority date | — |
| Expiry date | Apr 7, 2026 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3604
- 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.A specifier can give a method a plug-in pre- and postcondition, 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.