A tool for advanced static error detection using program verification technology with automatic theorem prover. Programmer specifies pre/post-conditions and invariants in comments of the Java program. They are similar to asserts, with the difference that the source is checked for validity only statically.

-- NikolaToshev

''Is this synonymous with as StaticAnalysis?''

----

CategoryLanguageTyping