Coding Rule Checking

November 18, 2008

Guillem Marpons


Coding Rule Checking

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Coding rules are often used in industry to codify software best practises and avoid the many hazardous constructions present in languages such as C or C++. Rules might also be devised to adapt programs to the available resources in specific execution environments. Predictable and customisable tools are needed to automatically measure adherence to these rules.

Many rules can be reformulated as logic programs, which provides both a framework for formal rule definition and a procedure for automatic rule conformance checking using a Prolog engine. Those properties of the software to be analysed involved in rule definition need to be transcribed into the same formalism used in rule specification. In our prototype, This is performed during normal compilation with a modified version of the GCC compiler.

We are working on the definition of a completely declarative logic-based language that facilitates the definition of new rules and the formalisation of some wide-spread rule sets. It will need to be expressive enough to codify the many program properties these rules rely on, and to accommodate some of the many analyses computed by modern compilers.