piątek, 8 października 2010

postcondition verification

Hello reader!

I have just made a program that takes a function or method signature with comments and generates a function that verifies postconditions of the function.
Download here(windows only so far). Click "Download 'cppAutoPostCon.exe' to your computer" at the bottom of the page.
Source here. Note that the only piece of code which is not inter platform is in the clipboard.cpp file. Feel free to port the code or use it for any purpose. Also note that with the source comes a project file for Code::Blocks IDE. Consult it if you want to build the code yourself because the set up is not trivial. Also note that the code has been compiled with GCC 4.4.1 and requires the Boost library v. 1.43.0 to be installed.

For example, it turns this:

//some text
//{{{ { a_setting_stuff ;;; a} {b}
// {c_setting_stuff ;;; c} }}}
///some more text
ret_type do_sth(arg1,arg2,arg3)

into this:

bool verify_do_sth(ret_type _result,arg1,arg2,arg3)
{
{
a_setting_stuff;
if(!(a))
return false;
}
if(!(b))
return false;
{
c_setting_stuff;
if(!(c))
return false;
}
return true;
}


Usage:
In your text editor select a function header with a comment.
Copy it to clipboard.
Run the program. (It will end in fraction of a second.)
The resulting verification function is now in the clipboard.
If the function could not be generated, the clipboard contains C++-style comment with an appropriate error message.

//edit 9th October
Now the program does much better job at formatting generated code, so that no line is too long to be legible and the indentation is acceptable.

Have fun verifying results of your function calls! (Yes, I know it sounds ridiculous. But the program is useful anyway.)

Brak komentarzy:

Prześlij komentarz