Performance-impacting postconditions

Declaring preconditions, postconditions, and invariants, and actually checking them at runtime are two different things.

For example Ada 2012 allows you to write:

   -- ...
   procedure Sort (Data : in out Array_Of_Something)
     with Post => (for all I in Data'First .. Data'Last - 1 =>
                     Data (I) < Data (I + 1)) is
   begin
      -- ... e.g. quicksort ...
   end Sort;

So we know that when Sort ends, the array Data must be sorted in ascending order (the aspect Post says us so). This is the “contract” for the procedure. Performing this check is Θ(N), so after all we are making Sort less efficient (quicksort is Θ(nlog(n))).

Maybe we want to state that postcondition, but also we don't want the actual runtime check is done when the code is released.

Anyway, no checks are performed if you don't add the following pragma:

   pragma Assertion_Policy (Check);

Or use the correct switch on the command line (-gnata; the pragma overrides the switch).

Maybe having them checked makes sense during the verification/validation steps of the software; keeping them makes sense whenever it is needed and the performance impact is well known, negligible, and affordable (the lesser of several evils principle?). No reason to keep checking code which shouldn't intervene, though. So, when is whenever it is needed?

I suppose the answer is in the following section.

Static and dynamic

Emphasis added:

The fact that specifications have the same meaning in proofs and during execution is very useful for debugging specifications: a run-time failure during testing might reveal that a precondition is wrong, and then classical debugging can be used to understand the failure. This perfect match between dynamic and static interpretation of specifications is also the basis for the combination of formal validation and testing. This allows discharging by testing the assumptions made during formal validation, when a program is only partially proved. These assumptions may be both contracts written by the user (preconditions and postconditions) that need to be exercised during testing, or implicit contracts added by the proof tools concerning initialization of subprogram inputs/outputs and non-aliasing properties. Under special switches, the GNAT compiler inserts the corresponding checks for these implicit contracts, so that they can too be verified dynamically during testing.

Then:

All the contracts have been checked by dynamic testing. This phase is quite classical, except for the fact that the testing includes the preconditions and the postconditions defined in the case study.

Taken from here.

And after that…

Yet, a failure like the one of Schiaparelli may still happen, no matter what. The probability of something bad happening is reduced, but this doesn't mean that something bad won't happen. Once something happens, its probability in the past knowing the future is still 1. (What is it supposed to mean is left to the reader.)