InterruptExit に事前条件がない

• Reporter: t-hori
• Owner: (del#7373)
• Type: Bugs
• Status: Open [Owner assigned]
• Component: (None)
• MileStone: (None)
• Priority: 5 - Medium
• Severity: 5 - Medium
• Resolution: None
• File: None

Details Reply

InterruptExit (section Target 内)の操作後に、intnest < 0 になってしまう可能性がある。適切な事前条件(例えば intnest > 0) を付与する必要があるのではないか。

Ticket History (2/2 Histories)

2009-05-21 16:34 Updated by: t-hori

• New Ticket "InterruptExit に事前条件がない" created

2009-05-27 18:22 Updated by: (del#7373)

• Owner Update from (None) to nsaito

Comment Reply

操作スキーマに記述するのは事後条件であり， 事前条件は pre 演算子を用いて計算し， それを仕様に記述する，ということになると思います．

今後の作業で操作スキーマに対する事前条件を計算の上， 明記するようにしたいと思います．