時相特性
時相特性(temporal property)
アルゴリズムのありとあらゆる「ライフタイム」(最初から最後まで)がシーケンスのさまざまな状態を互いに結びつける何かに従うことを検査する。
データベースで言うと、「常に整合性のとれた状態である」ことの検査と、「最終的に整合性がとれた状態になる」ことの検査の違いのようなもの
「口座の最終的な残高は開始時点の残高と同じである」要件が関連
(ref
『実践TLA+』
39P)