J
James Kanze
Name three.
If a shop does this - uses those methods to prove that their
software works - then i'm happy to call them software
engineers. Ecstatic, in fact - it's a great and wonderful
achievement.
But i believe that the number of such shops is vanishingly
small, and concentrated in a few sectors where the cost is
worth it - real-time control, telecoms, aerospace, defence,
medical devices. It's not a technique that is used for the
common bulk of software - desktop apps, web apps, even
operating systems. Furthermore, i don't believe it can be,
because such systems tend to be complex enough that the cost
of proving correctness would be so astronomical that it
wouldn't be economical.
First, a major part of engineering is being cost effective, and
not over-designing. Complete formal proofs are rarely used, at
least in the fields I've been active in (and that includes
telecoms and locomotive brake systems). Informal proofs,
evaluated during code review, are a normal part of any good
software development process, however. And for what it's worth;
one of the companies I worked for introduced the SEI methods
because of reliability constraints, only to find out that it's
actually cheaper to develop code that way.