Support for C++20 design by contract #6702
Description
Contracts have been voted into C++20 such that you may now write code like:
void push(int x, queue & q)
[[expects: !q.full()]]
[[ensures: !q.empty()]]
{
//...
[[assert: q.is_valid()]];
//...
}
At present we use @pre and @post & @invariant tags to document contracts using Doxygen.
This leads to the following feature request:
- Doxygen should parse expects and ensures attributes and treat them exactly as if I'd written:
///
/// @pre
/// @code !q.full() @endcode
///
/// @post
/// @code !q.empty() @endcode
///
void push(int x, queue & q)
[[expects: !q.full()]]
[[ensures: !q.empty()]]
{
//...
[[assert: q.is_valid()]];
//...
}
-
Doxygen should consider using @expects and @ensures as aliases or replacements for @pre and @post.
There is still a place for hand documented contracts (i.e current usage) even with C++20.
Some contracts are hard to express in code. Adding commentary to a contract to explain it can be useful. -
Doxygen might also consider adding an alternative way to literately document attributes with a more compact syntax. E.g.
void push(int x, queue & q)
[[expects: !q.full()]] /// the queue must not be full
[[ensures: !q.empty()]] /// following the operation the qeue cannot be empty
Might be equivalent to:
///
/// @pre
/// The queue must not be full
/// @code !q.full() @endcode
///
/// @post
/// Following the operation the qeue cannot be empty.
/// @code !q.empty() @endcode
///
void push(int x, queue & q)
[[expects: !q.full()]]
[[ensures: !q.empty()]]