A few summers ago I was an intern at JPL working on a static analysis suite for this exact standard.
Writing code checkers for these sorts of rules is a really interesting exercise and it helped me grow a lot as a programmer! I went from having no exposure to formal languages, parsing, and grammars to actively playing around with these concepts to try and help build more reliable software. It was a humbling, challenging, and incredibly rewarding experience.
Sometimes, a rule is extremely simple to implement. For example, checking a rule that requires that an assert is raised after every so many lines within a given scope is just a matter of picking the right sed expression. Other times, you really need an AST to be able to do anything at all.
A rule like "In compound expressions with multiple sub-expressions the intended
order of evaluation shall be made explicit with parentheses" is particularly challenging. I spent a few weeks on this rule! I was banging my head, trying to learn the fundamentals of parsing languages, spending my hours diving into wikipedia articles and learning lex and yacc. The grad students at LaRS were always extremely helpful and were always willing to help tutor me and teach me what I needed to learn (hi mihai and cheng if you're reading!). After consulting them and scratching our heads for a while, we figured we might be able to do it with a shift-reduce parser when a shift or reduce ambiguity is introduced during the course of parsing a source code file. This proved beyond the scope of what I'd be able to do within an internship, but it helped me appreciate the nuance and complexity hidden within even seemingly simple statements about language properties.
Automated analysis of these rules gives you a really good appreciation of the Chomsky language hierarchy because the goal is always to create the simplest possible checker you can reliably show is able to accurately cover all the possible cases. Sometimes that is simple as a regular language, but the next rule might require you to have a parser for the language.
For what it's worth, this is only one of the ways the guys at LaRS (http://lars-lab.jpl.nasa.gov/) help try to improve software reliability on-lab. Most of the members are world-class experts in formal verification analysis and try to integrate their knowledge with missions as effectively as possible. Sometimes, this means riding the dual responsibility of functioning as a researcher and a embedded flight software engineer, working alongside the rest of the team.
If anyone's interested in trying out static analysis of C on your own, I highly reccomend checking out Eli Bendersky's awesome C parser for Python (http://code.google.com/p/pycparser/). I found it leaps and bounds better than the existing closed-source toolsets we had licenses for, like Coverity Extend. At the time, it had the extremely horrible limitation of only parsing ANSI 89, but Eli has since improved the parser to have ANSI 99 compliance. Analyzing C in Python is a dream.
Gerard Holzmann (http://spinroot.com/gerard/) came to JPL from Bell Labs in 2003, and the period since he arrived has coincided with a time of greater prominence for methodologies of producing reliable software. Although many people contributed to the document in this post (see page 5), Gerard was the driving force behind drafting it and getting buy-in from the people who write flight software. The latter part -- cultural -- is as big a challenge as the technical stuff.
Another thing that happened around this time is getting licensing for Coverity and other tools, and introduction and promotion of static code verification, even for non-flight software.
> A rule like "In compound expressions with multiple sub-expressions the intended order of evaluation shall be made explicit with parentheses" is particularly challenging. I spent a few weeks on this rule! I was banging my head, trying to learn the fundamentals of parsing languages, spending my hours diving into wikipedia articles and learning lex and yacc.
Hmmm....how about this? If the code is parenthesized enough, then the precedence and associativity of the operators has no effect on the shape of the parse tree. So, if you take the expression and repeatedly make random changes to the operators and parse it, and you keep getting the same shape for the parse tree, it is sufficiently parenthesized.
I thought the sometimes-required-parentheses rule was interesting. Here's what I came up with in 30 minutes using ANTLR. Highly recommend it! The ANTLRWorks grammar IDE is incredibly useful -- it shows rules and trees visually, and can single-step the generated code so you can see your parse tree being built one token at a time.
The following grammar accepts input like 3 + (5 * 7) but rejects 3 + 5 * 7.
The key is that, if your expression doesn't start with a parenthesis, you know that all the operators at that level have to be the same. (I assume that sums or products of several things like 1 + 5 + (2 * 3) are permitted without parenthesizing further.)
Also, tool choice matters. ANTLR is an LL parser and Yacc/Bison are LR parsers; IMHO with LL it's much easier to understand what's going on. This grammar would need substantial rewriting for Yacc to deal with the fundamental differences between LL and LR parsing.
(edited to deal with HN markup issues related to asterisks and fix implementation bugs)
Writing code checkers for these sorts of rules is a really interesting exercise and it helped me grow a lot as a programmer! I went from having no exposure to formal languages, parsing, and grammars to actively playing around with these concepts to try and help build more reliable software. It was a humbling, challenging, and incredibly rewarding experience.
Sometimes, a rule is extremely simple to implement. For example, checking a rule that requires that an assert is raised after every so many lines within a given scope is just a matter of picking the right sed expression. Other times, you really need an AST to be able to do anything at all.
A rule like "In compound expressions with multiple sub-expressions the intended order of evaluation shall be made explicit with parentheses" is particularly challenging. I spent a few weeks on this rule! I was banging my head, trying to learn the fundamentals of parsing languages, spending my hours diving into wikipedia articles and learning lex and yacc. The grad students at LaRS were always extremely helpful and were always willing to help tutor me and teach me what I needed to learn (hi mihai and cheng if you're reading!). After consulting them and scratching our heads for a while, we figured we might be able to do it with a shift-reduce parser when a shift or reduce ambiguity is introduced during the course of parsing a source code file. This proved beyond the scope of what I'd be able to do within an internship, but it helped me appreciate the nuance and complexity hidden within even seemingly simple statements about language properties.
Automated analysis of these rules gives you a really good appreciation of the Chomsky language hierarchy because the goal is always to create the simplest possible checker you can reliably show is able to accurately cover all the possible cases. Sometimes that is simple as a regular language, but the next rule might require you to have a parser for the language.
For what it's worth, this is only one of the ways the guys at LaRS (http://lars-lab.jpl.nasa.gov/) help try to improve software reliability on-lab. Most of the members are world-class experts in formal verification analysis and try to integrate their knowledge with missions as effectively as possible. Sometimes, this means riding the dual responsibility of functioning as a researcher and a embedded flight software engineer, working alongside the rest of the team.
If anyone's interested in trying out static analysis of C on your own, I highly reccomend checking out Eli Bendersky's awesome C parser for Python (http://code.google.com/p/pycparser/). I found it leaps and bounds better than the existing closed-source toolsets we had licenses for, like Coverity Extend. At the time, it had the extremely horrible limitation of only parsing ANSI 89, but Eli has since improved the parser to have ANSI 99 compliance. Analyzing C in Python is a dream.