c3lang
Post/pre conditions
/**
* @param [inout] foo `test`
* @require baz > 100 `whatever`
* @ensure return < 200
*/
fn int test2(int *foo, int baz)
{
*foo = 444;
return baz;
}
Why /*...*/ is needed? It's bad for syntax highlighting in editors/IDE.
@param [inout] foo `test`
@require baz > 100 `whatever`
@ensure return < 200
fn int test2(int *foo, int baz)
{
*foo = 444;
return baz;
}
fn int test2(int *foo, int baz)
@param [inout] foo `test`
@require baz > 100 `whatever`
@ensure return < 200
{
*foo = 444;
return baz;
}
fn int test2(inout int *foo, int baz @require > 100)
{
*foo = 444;
return @ensure(baz < 200);
}
Also I found the bug. This cannot be compiled:
/**
* @param [inout] foo `test`
* @require baz > 100 `whatever`
* @ensure *foo > 231
* aaa_or_any_other_chars
*/
fn void test(int *foo, int baz)
{
}
fn void main()
{
}
Where would the function description be placed?
After [1] or before [2] contracts. Or some mixed approach [3].
I'll fix the bug. But [1] [2] [3] all seem to assume that doc descriptions then are separate.
Just for the note: @ used for attributes but @require, @ensure and @param aren't in c3c --list-attributes and c3c --list-keywords lists.
Maybe to use $ instead of @?
The simple code:
/**
* @require baz > 100
*/
fn void test(int baz)
{
}
fn void main()
{
test(10);
}
test: Assertion `@require "baz > 100" violated.' failed.
It's ok for the debug mode. But
Segmentation fault
for the release modes.
Yes, what happens here is that the optimizing backend finds out that the program will violate constraints and everything results in segmentation fault.
Regarding the keywords, the doc attributes are separate from normal attributes and are not reserved elsewhere.
[1] and [2] work for the preconditions but do not extend to any documentation.
[3] does not work for several cases:
- It is not implementing the ensure contract, since such a contract is to be true for all returns and associated with the function declaration. Otherwise there is no difference with an assert.
- Putting constraints next to the parameters do not scale. It's barely bearable for a single constraint, but for anything non trivial it just makes the function declaration look like it has cancer (compare C++ templates)