If nagini is eventually used, then the documentation needs to be updated.

[saltiniroberto]

If nagini is eventually adopted to express pre and postconditions (see PR #20 ), then the documentation must indicate that nagini has been used for specification purposes only. The spec is not expected to be verifiable by the nagini tool.