1
$\begingroup$

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

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ JML is not a tool, it is a language. $\endgroup$
    – Dave Clarke
    Commented Mar 21, 2013 at 13:33
  • $\begingroup$ 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? $\endgroup$
    – mrsteve
    Commented Mar 21, 2013 at 16:31
  • 1
    $\begingroup$ 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. $\endgroup$
    – Dave Clarke
    Commented Mar 21, 2013 at 16:36

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – mrsteve
    Commented Mar 21, 2013 at 16:44
  • $\begingroup$ 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". $\endgroup$
    – mrsteve
    Commented Mar 21, 2013 at 16:50
  • $\begingroup$ 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. $\endgroup$
    – Vijay D
    Commented Mar 22, 2013 at 16:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.