<p>This is a strange comparison. Your question is comparable to asking "how expressive is the ANSI C language specification compared to stdlib and compilation". The comparisons don't make sense.</p>

<ol>
<li>The Java Modelling Language can be used as a specification language to specify properties of code. The language alone does not solve the problem of verifying whether these properties are satisfied.</li>
<li>A model checker allows you to check if a system with a transition system semantics satisfies a logical formula. The formula is typically written in a propositional temporal or modal logic though first-order and other extensions exist. Nonetheless, most model checkers used in practice do not support specification languages with quantifiers. I do not know of a model checker that supports a specification language as rich as JML. </li>
<li>A certified library contains code that provides certain guarantees. Those guarantees may have been provided using a theorem prover, or a model checker, or by doing a  manual proof. </li>
</ol>

<p>If you want a mathematical comparison, to me, it's like comparing the formulae of first order arithmetic (a language), the principle of induction (a proof technique) and a collection of theorems in a number theory textbook. They are related concepts but they do not achieve the same goal so comparing them does not make sense. </p>

CC BY-SA 3.0
2013-03-21T16:44:28.483Z
Thank you for you question. Although I am quite sure because of my conversation with two professors in that field. Model Checking is a kind of verification technique that cannot be used for software certification. You cannot proof anything with a model checker, in order to do that you would need to extract a formal proof, say in Coq, from the output of the model checker. The model checker could be faulty and therfore software certification is not possible. In contrary, with Coq you can print the proof, check it by hand, possibly feed it into another theorem prover like Agda, etc.
mrsteve
CC BY-SA 3.0
2013-03-21T16:50:02.723Z
My misconception was about "The language alone does not solve the problem of verifying whether these properties are satisfied.". anyway, I voted the answer up and can accept it later... Perhaps there are also multiple definitions of "certified software".
mrsteve
CC BY-SA 3.0
2013-03-22T16:53:58.123Z
I disagree with both the statements being made about model checking but this comment is not the best place to explain. Maybe you can make a separate question with that text asking if model checkers can be used for software certification, or comparing model checkers and Coq. I will write a full answer there.
Vijay D
CC BY-SA 3.0
2013-03-21T16:34:48.553Z
2013-03-21T16:34:48.553Z
Vijay D
<p>(note: this is probably a beginner question, and English is not my first language)</p>

<p>Recently, I have read a paper that used the “Java Modeling Language” (JML), see for instance:</p>

<p><a href="http://www.eecs.ucf.edu/~leavens/JML//index.shtml" rel="nofollow">http://www.eecs.ucf.edu/~leavens/JML//index.shtml</a><br>
<a href="http://www.eecs.ucf.edu/~leavens/JML/fmco.pdf" rel="nofollow">http://www.eecs.ucf.edu/~leavens/JML/fmco.pdf</a>  </p>

<p>a) certified Software<br>
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.</p>

<p>b) model checking<br>
software verified via model checking is not certified or formally verified software, as the model checker has to be trusted.</p>

<p>How does the "Java Modeling Language" (JML) compare for verification purposes?</p>

<p>Okay, I think I get it. It is not about software verification, as it is stated that:</p>

<p>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 <strong>while the
program is running can be detected immediately.</strong></p>

<p>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. </p>

CC BY-SA 3.0
2013-03-21T13:33:25.283Z
JML is not a tool, it is a language.
Dave Clarke
CC BY-SA 3.0
2013-03-21T16:31:23.183Z
thank you for the comment, it got me thinking again. Any ideas, should I just delete the question or close it otherwise? Answer my own question?
mrsteve
CC BY-SA 3.0
2013-03-21T16:36:49.300Z
If you have an answer to your own question, you may provide it. Or you could rephrase the question to talk about tools in the JML space.
Dave Clarke
<pl.programming-languages><program-verification><formal-methods><se.software-engineering>
Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?
mrsteve
# Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?

(Asked by: username_0 on 2013-03-21)

(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:

<http://www.eecs.ucf.edu/~leavens/JML//index.shtml>  
<http://www.eecs.ucf.edu/~leavens/JML/fmco.pdf>

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.

**Tags:** pl.programming-languages, program-verification, formal-methods, se.software-engineering

> **Comments:**
> **username_1**: JML is not a tool, it is a language.  
> **username_0**: thank you for the comment, it got me thinking again. Any ideas, should I just delete the question or close it otherwise? Answer my own question?  
> **username_1**: If you have an answer to your own question, you may provide it. Or you could rephrase the question to talk about tools in the JML space.  

---

## 1 answers

### Answer by username_2 on 2013-03-21. Score: 3 | Accepted answer

This is a strange comparison. Your question is comparable to asking "how expressive is the ANSI C language specification compared to stdlib and compilation". The comparisons don't make sense.

1. The Java Modelling Language can be used as a specification language to specify properties of code. The language alone does not solve the problem of verifying whether these properties are satisfied.
2. A model checker allows you to check if a system with a transition system semantics satisfies a logical formula. The formula is typically written in a propositional temporal or modal logic though first-order and other extensions exist. Nonetheless, most model checkers used in practice do not support specification languages with quantifiers. I do not know of a model checker that supports a specification language as rich as JML.
3. A certified library contains code that provides certain guarantees. Those guarantees may have been provided using a theorem prover, or a model checker, or by doing a manual proof.

If you want a mathematical comparison, to me, it's like comparing the formulae of first order arithmetic (a language), the principle of induction (a proof technique) and a collection of theorems in a number theory textbook. They are related concepts but they do not achieve the same goal so comparing them does not make sense.

> **Comments:**
> **username_0**: Thank you for you question. Although I am quite sure because of my conversation with two professors in that field. Model Checking is a kind of verification technique that cannot be used for software certification. You cannot proof anything with a model checker, in order to do that you would need to extract a formal proof, say in Coq, from the output of the model checker. The model checker could be faulty and therfore software certification is not possible. In contrary, with Coq you can print the proof, check it by hand, possibly feed it into another theorem prover like Agda, etc.  
> **username_0**: My misconception was about "The language alone does not solve the problem of verifying whether these properties are satisfied.". anyway, I voted the answer up and can accept it later... Perhaps there are also multiple definitions of "certified software".  
> **username_2**: I disagree with both the statements being made about model checking but this comment is not the best place to explain. Maybe you can make a separate question with that text asking if model checkers can be used for software certification, or comparing model checkers and Coq. I will write a full answer there.  

---

