Re: Proposal: pragma Assumption

["Santiago Urueña" <suruena@gmail.com>]

> I've been using pragma Fixme; for this -- OK, won't fail in production
> (unless you use GNAT & -gnatwe, treat warnings as errors, or your
> compiler's equivalent).
>
Interesting, that's very close to this type of assertions (except that
it doesn't document much, and it won't fail if any test tries to
exercise the unimplemented code). Which compiler has that pragma?

http://www.adacore.com/wp-content/files/auto_update/gnat-unw-docs/html/gnat_rm_2.html

Currently GNAT has the following related pragmas, but none is close to
pragma Fixme or Assumption:

 pragma Assert (boolean_EXPRESSION [, string_EXPRESSION]);
 pragma Check (
     [Name    =>] Identifier,
     [Check   =>] Boolean_EXPRESSION
  [, [Message =>] string_EXPRESSION] );
 pragma Check_Name (check_name_IDENTIFIER);
 pragma Check_Policy ([Name =>] Identifier, CHECK|IGNORE);

 pragma Compile_Time_Error
         (boolean_EXPRESSION, static_string_EXPRESSION);
 pragma Compile_Time_Warning
         (boolean_EXPRESSION, static_string_EXPRESSION);

 pragma Debug ([CONDITION, ]PROCEDURE_CALL_WITHOUT_SEMICOLON);
 pragma Debug_Policy (CHECK | IGNORE);

 pragma Postcondition (
   [Check   =>] Boolean_Expression
 [,[Message =>] String_Expression]);
 pragma Precondition (
   [Check   =>] Boolean_Expression
 [,[Message =>] String_Expression]);


Pragma Assert, Check (generalization of Assert), Debug, Postcondition
and Postcondition are evaluated at run-time, but are intended for the
whole life of the application. In contrast, pragma Compile_Time_Error
and Compile_Time_Warning are evaluated at compilation time (mainly to
detect assertion errors when instantiating a generic), so cannot be
equivalent to pragma Assumption.


Regards,

--
Santiago Urueña-Pascual
Technical University of Madrid (UPM)