Hi everybody,
I'm thinking in sending the following proposal to the ARG, but I'd
like to present it here first to have more opinions about it
usefulness, and probably to refine it a bit with your comments...
It is based on a 2004 paper of Tony Hoare (from the book 'From Object-
orientation To Formal Methods') where he describes different types of
assertions used by (C/C++) developers in production code, including
this one:
SYMPLIFYING_ASSUMPTION (strlen(input) > MAX_PATH, "not yet checking
for overflow");
'SYMPLIFYING_ASSUMPTION' is a macro very similar to the C 'assert',
also checking at run-time a boolean condition and aborting the program
if it evaluates to false. But if an 'assert' is valid during the whole
life of the application, the 'SYMPLIFYING_ASSUMPTION' is used by the
programmer just *during the coding phase* to do***ent those cases that
aren't coded yet (probably edge cases). The difference is when
compiling the program _not_ in debug mode (NDEBUG defined): the
'assert' macros are eliminated by the preprocessor whereas it is a
compilation error if any 'SYMPLIFYING_ASSUMPTION' remains in the
sources.
That is, a SYMPLIFYING_ASSUMPTION is like those 'TODO:' or 'FIXME:'
annotations used to remind the programmer what should be modified in
the code, but it is recognized by the compiler instead of being just a
comment, and therefore cannot be ignored by accident.
So the proposal whould be adding to the next Ada revision two new
pragmas:
pragma Assumption ([Check =3D>] boolean_expression[, [Message =3D>]
string_expression]);
pragma Assumption_Policy (policy_identifier); -- Error, Check
Which behave exactly like Assert and Assertion_Policy (also raising
Assertion_Error, but with a different message), except that by default
it is a compilation error to find any pragma Assumption in the sources
unless when explicitly allowed using a compilation flag or the 'Check'
policy.
Probably better names can be chosen for those pragmas, so feel free to
propose more adequate identifiers. Also, maybe in this case the
Message string should be required, anyway it is a do***entation pragma
(in pragma Assert the second parameter is optional).
IMHO this pragma is not a complete replacement for the TODO or FIXME
comments, and in many cases it is better to code the whole
functionality at once than just the more common cases. However,
sometimes it will be a good approach to code just some cases
do***enting the assumptions, run the testsuite (raising an exception
if any of those missing cases are triggered), and to code the rest in
the future. But now, even if you forget to add that code, the compiler
will remind you about those missing cases when trying to compile the
final executable (following the "programmers make faults" Ada
philosophy).
Do you think it is an useful addition to Ada 2015? Would you use this
feature? Do you know of any means to achieve the same effect in Ada
2005? Thanks
Cheers,
--
Santiago Urue=F1a-Pascual
Technical University of Madrid (UPM)
|
