global invariant

глобальный инвариант (предикат, истинный в каждом видимом состоянии программы, а именно, до и после каждого неделимого действия ssn)