看起来C语言对于在代码中使用的形式化方法具有良好的支持(frama-c、VCC、verifast)。据我所知,C++似乎没有可比较的类似支持。 有哪些形式化方法可用于推理关于采用C++编写的安全关键软件的相关问题?
我与一家医疗公司合作,他们使用Coverity和Klocwork检查代码是否存在潜在问题,例如资源泄漏和未初始化指针的使用。然而,这些只是工具,并非安全关键代码的标准。我看到MISRA正在制定C++标准。他们早先从C开始,大约5年前开始着手C++。一个大问题是MISRA C++标准规定不得使用模板。这实际上限制了你在C++中所能做的事情。但是,你可以将该文档用作起点。例如,你可能希望将软件中使用的模板限制为标准库和boost。请注意,Klocwork有一个MISRA C++扩展。然而,编写良好的代码的最佳方法之一是使用单元测试和集成测试进行测试。多年来,我发现这比大多数其他方法更可靠。