InterruptExit に事前条件がない
InterruptExit (section Target 内)の操作後に、intnest < 0 になってしまう可能性がある。適切な事前条件(例えば intnest > 0) を付与する必要があるのではないか。
操作スキーマに記述するのは事後条件であり， 事前条件は pre 演算子を用いて計算し， それを仕様に記述する，ということになると思います．
今後の作業で操作スキーマに対する事前条件を計算の上， 明記するようにしたいと思います．
InterruptExit (section Target 内)の操作後に、intnest < 0 になってしまう可能性がある。適切な事前条件(例えば intnest > 0) を付与する必要があるのではないか。