I was throwing something together recently, and realized none of my Pre and Post conditions were being caught.
Why is -gnata not enabled by default in new projects?
In some situations it might cause unwanted exceptions, such as spark mode or zfp runtimes but I do not think that is the reason. Spark code often has pragmas for assertions off anyway
I believe the gnat studio interface might mention performance reasons and suggest that you may want to choose certain options instead of enabling all with -gnata.
Sorry. Now that I am in front of gnat studio. I realise I was thinking of -gnatVa providing many options.
Personally I want Ada assertions off and I am looking into SPARK static checks. I can only guess it is possibly because of performance and more likely a library or program may have checks that are only meant for debugging and a user may just want to compile it and not develop it.
One minute later I read that assertions may be useful during testing to check proofs that could not be completed.
I guess if you want to ensure that they are compiled in at release as ada contract checks then the pragma might be a better idea. Though, I guess that you are talking about Alire development mode.
To quote from “building high integrity applications with spark”
assertions have the potential to slow down programs by a huge factor…assertions could make the difference between meeting performance goals and total unusability.
For this reason some compilers, such as GNAT, do not execute assertions by default.
True, for e.g. for all El of Some_Loaded_Container => Some_Complex_Test (El) (I’ve temporarily (I hope) forgotten the technical term 
)
The assertions are enabled in the validation profile. The rationale is not explicit in the Alire documentation, nor in the GitHub issues and pull-requests [1] [2], but I gather it is:
- Validation: I don’t mind how slow is either the compilation or the program itself, I want to have as many compile-time and run-time checks as possible to validate the program.
- Development (default): I want quick development cycle, reduce compile time and I don’t mind if the program is not as fast as possible.
- Release: I’ve finished development and validation. I don’t mind how slow is the compilation, but I want the final program to be as fast as possible while preserving the standard Ada run-time checks.
2 Likes
Ada unit testing requires more setup than other languages – at least without GNAT studio.
So when sketching out ideas in prototypes, using Pre/Post/*_Predicate/Invariant helps catch incompatible changes and mistakes very quickly, which was my situation.
In general, in other languages and environments, I expect assertions/extra checks in debug (i.e. validation) or development modes of programs, but not running in release mode. Example of what UE5 does.
It’s nice to have “development” asserts and “known-slow, but only in debug mode” asserts, with release versions of apps shipping with extremely few, if any, assertions. Assertion_Policy seems like it could help in the “I need to debug this” scenario, but I think you only get granularity of enabling or disabling each category in a compilation unit.
If your subprogram has a precondition, you have to specify that precondition to its users. Then you either have to show that it can never be called in violation of its precondition, or you have to test the precondition at run time. In some cases, such as reusable components, you cannot show that the precondition can never be violated, so a run-time test is essential.
The Pre => precondition syntax is a useful way to specify preconditions, and the automatic run-time tests of preconditions is a good way to have run-time tests when needed. If you plan to disable assertion tests in the deployed S/W, then you have to write the test in the subprogram, effectively duplicating the specification of the precondition. Duplicate code is generally a bad thing.
So, except when using SPARK, I write preconditions using Pre => and leave assertion tests on at all times. Otherwise, I cannot have confidence that my S/W is correct.
Of course there are cases where preconditions cannot be written using Pre => and cannot be tested except in the subprogram body, where the body will essentially duplicate the precondition test, and where the test is too time-consuming to implement and you have to warn your users of this in big, flashing, red letters. In those cases it’s probably best to not use Pre => and to fall back on comments and a test in the body (if reasonable). But such cases are rare.
Exactly this.
@pyj we started with all checks enabled but in some cases the performance price is just too high and can make your program unusable even for just testing it.