Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?
(note: this is probably a beginner question, and English is not my first language)
Recently, I have read a paper that used the “Java Modeling Language” (JML), see for instance:
a) certified Software
To my understanding, a sorting algorithm proven correct in the theorem prover Coq (and possibly extracted to an ocaml program) is “certified software” or formally verified software, as a mathematical proof of the correctness can be extracted and possibly manually verified.
b) model checking
software verified via model checking is not certified or formally verified software, as the model checker has to be trusted.
How does the “Java Modeling Language” (JML) compare for verification purposes?
Okay, I think I get it. It is not about software verification, as it is stated that:
The contracts are defined by program code
in the programming language itself, and are trans-
lated into executable code by the compiler. Thus,
any violation of the contract that occurs while the
program is running can be detected immediately.
I cannot find a real example of verification in the above paper, at least not in the sense of model checking or certified software, so I guess they just don’t have an emphasis on formal methods.