Applying mathematical software documentation: an experience report

Those who do not use "formal methods" for developing software (and they remain the overwhelming majority of software developers) often claim that mathematical software development can only be used by highly educated people, and on especially well-written programs. We counter this claim by reporting on some recent experience. An undergraduate engineering student who had no previous exposure to mathematical software documentation techniques was asked to use a new method to document a program that had been written for photonics and microwave development, but did not always work as required; the author had departed and the program's owners were not able to find the problem. The student was not asked to change the program, just to provide precise documentation. However, the process of documentation revealed several errors and, after they were corrected, the program was left in working, and maintainable condition. Our experience supports the position of those who believe that mathematical methods can be used by typical engineers with immediate benefits.