形式上の区別
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/07/26 07:42 UTC 版)
安全性と有効性の区別は、 P ( t ) {\displaystyle P(t)} という述語によって形式的に確立することができる。 ここで、 t {\displaystyle t} は時間を意味する。 t 0 {\displaystyle t_{0}} をlivenessとsafetyの特性が評価される出発点となる瞬間とする。以下の例では、 x {\displaystyle x} をデッドロックフリーであることを保証したいプロセス（またはスレッド）とする。 安全性: ∀ t ≥ t 0 : P ( t ) = False . {\displaystyle \forall t\geq t_{0}:P(t)={\textrm {False}}.} 事例: P ( t ) {\displaystyle P(t)} は " x {\displaystyle x} が時間 t {\displaystyle t} でデッドロックの状態にある"ことを意味する。 ライブネス: ∀ t 1 ≥ t 0 , ∃ t ≥ t 1 , t < ∞ : P ( t ) = True . {\displaystyle \forall t_{1}\geq t_{0},\exists t\geq t_{1},t<\infty :P(t)={\textrm {True}}.} 事例: P ( t ) {\displaystyle P(t)} は " x {\displaystyle x} が時間 t {\displaystyle t} で待機、停止する"ことを意味する。
※この「形式上の区別」の解説は、「ライブネス」の解説の一部です。
「形式上の区別」を含む「ライブネス」の記事については、「ライブネス」の概要を参照ください。
- 形式上の区別のページへのリンク
