As with other Java assertion tools, the BSL assertion implementation acts as a preprocessor: it transforms the source code and embeds each enabled assertion using a Bandera library method Bandera.assert(boolean). A little bit of extra work is needed to maintain proper label correspondence in LOCATION assertions and to calculate the value of the variable $ret in POST assertions, but the transformation is otherwise straightforward. One can also hardcode assertions directly with Bandera.assert, but this is discouraged. When Bandera generates models for Spin, each Bandera.assert call is translated to a Promela ASSERT statement.