JPYCv2 形式検証

外観

JPYC.unpause_sets_unpaused ​

名称・種別 ​

  • 名称: JPYC.unpause_sets_unpaused
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:215-216
  • 概要: 成功した unpause は paused を false にする（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext}, Eq (JPYC.unpause s ctx) (Except.ok s') → Eq s'.paused Bool.false

unpause の成功は結果状態の paused を false にする、という効果定理です。

解説 ​

何を述べているか。 unpause が成功した結果状態では paused = false です。unpause_ok の結果状態から従います。

直感。 「解除ボタンで通常運転に戻る」を確認します。

なぜ安全性に効くか。 停止と解除が状態の真偽値を確実に切り替えるので、運転状態の遷移に曖昧さがありません。

図解 ​

Lean ソースコード ​

lean
theorem unpause_sets_unpaused {s s' : State} {ctx : CallContext} (h : unpause s ctx = .ok s') :
    s'.paused = false := by obtain ⟨_, rfl⟩ := unpause_ok h; rfl

依存 ​