Polyspace

複雑性クラスについては「PSPACE」をご覧ください。

Polyspaceは、静的コード解析ツール。C言語、C++、Adaのソースコードに実行時エラーが存在しないことを検出または証明するための抽象解釈による大規模分析ができる。このツールはソースコードが適切なコード標準に準拠しているかどうかもチェックできる。^[3]

Polyspace

開発元	MathWorks [1]
最新版	R2019a / 2019年3月15日 (6年前) (2019-03-15)
対応OS	クロスプラットフォーム[2]
種別	静的コード解析
ライセンス	Proprietary
公式サイト	www.mathworks.com/products/polyspace.html

一般的な利用法

Polyspaceはソースコードを調べて算術オーバーフロー、バッファオーバーラン、ゼロ除算などの潜在的なランタイムエラーが発生する可能性のある場所を特定する。ソフトウェア開発者と品質保証マネージャーは、この情報を使用して、コードのどの部分に欠陥があるか、または信頼できることが証明されているかを特定する。コードの他の部分は、証明されていないチェック用にマークされており、個別にレビューするべきである。^[4][5]

MISRA Cなどのコード標準またはコーディング規約はコードの品質、移植性、および信頼性に取り組もうとする。この製品はC言語およびC++のソースコードがこれらのコード標準のルールの一部に適合しているかどうかをチェックする。^[6]

Capabilities

The product family consists of Polyspace Code Prover and Polyspace Bug Finder. The Code Prover module annotates source code with a color-coding scheme to indicate the status of each element in the code.^[7] It uses formal methods-based static code analysis to verify program execution at the language level.^[5] The tool checks each code instruction by taking into account all possible values of every variable at every point in the code, providing a formal diagnostic for each operation in the code under both normal and abnormal usage conditions.^[8]

The Bug Finder module identifies software bugs by performing static program analysis on source code. It finds defects such as numerical computation, programming, memory, and other errors. It also produces software metrics such as Comment density of a source file, Cyclomatic complexity, Number of lines, parameters, call levels, etc. in a function, Identified run-time errors in the software.^[9]