Eiffel
#プログラミング言語
https://www.eiffel.org/
表明の表現
check：その他の表明
require：事前条件を表現
ensure：事後条件を表現
invariant：不変条件を表現
old：ルーチン呼び出し時の状態を取得するためのキーワード
ループ不変条件
実行時監視
no：なし
require：事前条件
ensure：事前条件+事後条件
invariant：事前条件+事後条件+クラス不変条件（開始時&終了時）
all：事前条件+事後条件+クラス不変条件（開始時&終了時）+check表明+ループ不変条件+ループ変化条件