tags:

views:

39

answers:

1
+1  Q: 

Java Modeling Language for C ?

Hi !

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.

A: 

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.

Pascal Cuoq  2010-10-13 12:48:44

related questions

any good tool for makefile generation?
How do you pass a function as a parameter in C?
Where should a veteran C programmer start in order to master Java ?
Any good book on best practice and guidelines in developing a SDK in C?
How do you determine the size of a file in C?
Decoding printf statements in C (Printf Primer)
Shift operator in C
How to avoid redefining VERSION, PACKAGE, etc.
Alpha blending sprites in Nintendo DS Homebrew
When should I use type abstraction in embedded systems
How to implement continuations?
What are the barriers to understanding pointers and what can be done to overcome them?
Anyone have experience creating a shared library in MATLAB?
String.indexOf function in C
Passing multidimensional arrays as function arguments in C
C/C++ library for reading MIDI signals from a USB MIDI device
Choosing a static code analysis tool
How do you printf an unsigned long long int?
Good STL-like library for C.
Rockbox audio format
Why am I getting a malloc: double free error with realloc()?
Should I learn C?
GTK implementation of MessageBox
Is gettimeofday() guaranteed to be of microsecond resolution?
How to use the C socket API in C++ on z/OS