An assertion facility provides a convenient way for a programmer to specify a constraint on a program's data space that should hold when control reaches a particular control location. In C and C++ programming, assertions are typically embedded directly in source code using an assert macro, where the location of the assertion is given by the position of the macro invocation in the source program.
Due to Java's support for extracting HTML documentation from
Java source code comments via Javadoc technologies,
several popular Java assertion facilities,
such as iContract [12],
support definition of assertions in Java method header comments. BSL
also adopts this approach. For example,
we saw in Section 5.6
the declaration of the BSL assertion
PRE PositiveBound: (b > 0).
In this assertion, the data constraint is (b > 0) and the
control location is specified by the occurrence of the tag
@assert PRE in the method header documentation for
BoundedBuffer constructor: the constraint must hold whenever control
is at the first executable statement in the constructor.