Статья 461

К инвариантным относятся свойства частичной корректности, взаимного исключения критических секций, отсутствия тупиковой ситуации, глобальные инварианты.
Частичная корректность. Пусть предусловие, некоторое ограничение, накладываемое на множество вводов, для которых данная программа полагается правильной, постусловие, выражающее тот факт, что программа выполняет задачу, ради решения которой создавалась.
Пусть исходные метки процессов параллельной программы конечные метки этих же процессов. Тогда частичная корректность данной программы относительно и может быть выражена следующей формулой.
Если программа, начавшаяся при соответствующих исходных условиях, выполняющих предусловие, завершается, то она завершается с правильным результатом, постусловие выполняется.
Свойство частичной корректности значимо и для последовательных, и для параллельных завершающихся программ.