JML annotations inside model methods are not translated. As an example, consider the following model method:
//@ assignable bank_spec;
//@ public model void update_tp_swiss() {
//@ if (never_called_update_tp_swiss) {
//@ set never_called_update_tp_swiss = false;
//@ set tp_swiss = false;
//@}
//@
//@ if (is_swissType) {
//@ set tp_swiss = true;.
