Статья 467

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

называются

называются


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