Java Modeling Language for C?

Question

I remember reading something about a formal specification language for C a while ago, but I can not find it now that I need it.

It was inspired by JML, using as far as I saw the same syntax.

The only reference to it I found is a paper, but what I am talking about was more polished than that.

If this rings a bell to you...

If nobody knows about this, I'll be happy to hear about a way to do formal verification and automatic test generation in C.

Thanks in advance.

Answer 1

I am not familiar with CML, but the article you link starts with the statement that it is for specification of non-functional requirements.

JML is for functional requirements of Java programs (okay, the line is blurry, but I think the CML article is using the word in the same sense as this sentence). An equivalent of JML for C programs (therefore also purely for functional requirements) is ACSL.

For formal verification, I can only recommend Frama-C (disclaimer: I work on Frama-C but not on a part that has to do with ACSL specifications). For test generation for C programs, I have heard good things about CUTE.

Answer 2

Formal specification "for" C?

I know of work to formally specify C: Denotational Semantics for C.

If you want to specify what C programs do, then the Property Specification Language might be a useful place to start.

Answer 3

There are at least 4 verification systems for C around:

1. Escher C Verifier. [I am connected with this.]
2. Microsoft VCC.
3. Frama-C with the Jessie plugin (available on Debian/Ubuntu in the package frama-c. You'll need to install why too to make jessie work)
4. VeriFast.

(1) is intended for safety-critical embedded C programs written in MISRA-C or similar. (2) is intended for multithreaded systems built using the Microsoft C compilers. I know rather less abiout (3) and (4).