Assertions

    Assertions are sometimes called preconditions or postconditions.  True assertions are Boolean tests conducted on data used in program variables.  In a design by contract approach to writing programs, assertions are used to test the data to make sure it is within the specifications for which the program has been written.  Assertions are used for data that is pasted from one program to another.  It is not used for data that is entered by a user.  Preconditions verify that data entering the program meets the specifications, while postconditions verify data leaving the program stays within the parameters for which the program was written.  Sometimes events happen during the execution of a program that are not part of the assertions that have been set forth.  These conditions are called exceptions.  Programmers need to anticipate any exceptions that will happen during the execution of their program.  Table 1 gives a comparison of Eiffel, Java, C++, and Ada 95.
 
 

Eiffel
Java
C++
Ada 95
Assertions
YES
NO
YES (LIMITED)
NO**
Exceptions
YES
YES
YES
YES
Table 1 Assertions and Exceptions

** SPARK Ada subset has assertions in the form of pre/post conditions, loop invariance ect. which are used to generate verification conditions allowing partial correctness to be established.  These are not checks which are monitored at run time.  For more information on the SPARK Ada subset, you can visit Praxis Critical Systems Ltd at  http://www.praxis-cs.co.uk/.

    C++ assertions are limited to keyword assert.  An assertion in C++ normally looks like

// assert: n >= 1

The '//' in the front of the word assert indicates that the line is a comment and performs no function except to inform the programmer.  This type of comment can be used in any programming language.

    Ada 95 does not have assertions like those found in Eiffel.  In Eiffel the keyword require is used for preconditions and ensure is used for postconditions.  An example is shown in Figure 1.
 

require
       I >= 1

ensure
       Output > 0
Figure 1 Eiffel example

    If the assertions are not true then the program is halted.  In Ada 95 a programmer can write his own exception which can perform the same function as an assertion.  An example is shown in Figure 2.
 
 

Bad_Output : exception;

begin

   ... -- code

   if Output < 1 then
   raise Bad_Output;
   end if;
end;
Figure 2 Ada 95 example

    Run-time checking for some exceptions that are built into Ada 95 can be turned off after a program has been tested and known to work properly.  The main reason a programmer will turn off some or all of the run-time checking is to maximize code efficiency by ignoring little error conditions, such as data out of range.  This should only be done after the programmer has performed extensive testing and the program is certified free from errors which would raise the exceptions detected by the run-time checking.

Note: The exceptions are still in the program.  They will never be raised after the run-time checking is shut off.

    Table 1 indicates that Ada 95 does not support assertions.  This is true for the language as a whole, but some compilers do have assertions in conjunction with pragmas.  An example of a pragma assert was given by Nick Roberts on the comp.lang.ada news group and is shown in Figure 3.
 
 

if not boolean_expression then
     pragma Assert (Expression_I_Expect_To_Be_True); -- pragma assert
-- pragma assert expanded
if not boolean_expression then
     Ada.Exceptions.Raise_Exception (
         Ada.Assertions.Assert_Failure'Identity,
         "Test expression evaluated to False in pragma Assert." & NL & 
         "Page: " & Page & "Line: " & Line & NL &
         "File: " & Source_File_Name & NL &
         [""|string_expression]);
end if;

-- NL is the implementation's code for a line break
_____________________________________________

package Ada.Assertions is
     Assert_Failure: exception (renames lower_level_exception);
end Ada.Assertions;
Figure 3  Pragma assertion example

 

Go to Encapsulation or the Table of Contents