9.6. Инвариантные свойства

Программные свцйства, которые всегда должны выполняться для данной программы, называют инвариантными свойствами. Они описываются формулой вида

Это означает, что формула должна быть истинна для каждой последовательности допустимого вычисления, определяемого начальными условиями этой формулы, т.е. — инвариант по отношению к такому допустимому вычислению (исходя из этого, можно было бы вместо написать

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

9.6.1. Частичная корректность

Это свойство имеет значение только для программ, в которых каждый процесс содержит терминальное место Такие программы назовем терминальными в отличие от нетерминальных программ, которые предполагают бесконечное выполнение и поэтому не содержат терминальных мест. Пусть — предусловие, которое задает ограничения на множество значений входных и программных переменных и переменных мест, для которого предполагается, что программа является правильной. — утверждение о корректности программы, т.е. отношение, которое должно установиться между входными переменными х и результирующими значениями у при приходе всех процессов в терминальные места. Используя введенные обозначения, свойство частичной корректности записывается следующим образом:

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

Пример. Программа вычисления факториала:

В результате выполнения этой программы после ее останова в месте иметьуг Утверждение частичной корректности для этой программы следующее:

где начальные условия, ассоциируемые с допустимым вычислением, имеют вид

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

Пример. Программа, подсчитывающая число вершин в двоичном дереве X:

проверка стека на наличие в нем вершин дерева X.

выбор головы голова и хвоста хвост стека и помещение их в соответственно.

проверка переменной дерева на отсутствие в нем вершин.

Увеличение счетчика на 1.

Помещение левого и правого поддеревьев в стек

Здесь Т — переменная дерева; — стек, содержащий вначале дерево X, состоящее из поддеревьев; голова — взятие головы стека хвост — взятие хвоста стека 5; левое — дает левое поддерево; — дает правое поддерево. Определяя как число вершин в дереве Т, можем выразить утверждение частичной корректности:

Начальные условия, соответствующие допустимому вычислению для этого случая, имеют вид

Пример. Параллельная программа вычисления биноминальных коэффициентов: Утверждение частичной корректности:

Полное начальное условие, ассоциируемое с допустимым вычислением:

9.6.2. Чистое поведение

Свойство чистого поведения обусловливает правильность выполнения переходов (команд) для каждого места процессов программы. Например, в случае деления свойство чистого поведения может обусловливать, что делитель не ноль и не слишком мал, чтобы не приводить к переполнению. Если программа содержит ссылку на элемент массива, то свойство чистого поведения может обусловливать попадание индекса в определенные границы. Обозначив условие чистого поведения в месте как будем иметь следующую запись свойства чистого поведения:

Конъюнкция берется по всем потенциально опасным местам программы.

Пример. Программа должна давать только целые числа в течение всего времени вычисления. Тогда условие чистого поведения для программы вычисления факториала в месте являющемся критическим, будет следующим:

Пример. Если программа деление содержит команду

где оператор целого деления и изменение индекса массива лежит в пределах от 1 до то условие чистого поведения в месте будет следующим:

Пример. Свойство чистого поведения для программы, считающей вершины дерева, имеет вид

Это утверждение гарантирует, что не будет сделана попытка вытолкнуть (взять) данные из пустого стека или декомпозировать пустое дерево.

Пример. Главное условие чистого поведения для программы вычисления биноминальных коэффициентов будет следующим:

9.6.3. Глобальная инвариантность

Очень часто некоторые свойства программ не зависят от какого-либо конкретного места. В этом случае говорят о глобальных инвариантностях. Свойство глобальной инвариантности в общем виде выглядит следующим образом:

т.е. свойство всегда имеет место в течение допустимого выполнения.

Пример. Условие того, что у, всегда должно быть положительным для программы вычисления факториала, выглядит следующим образом:

Другое условие глобальной инвариантности для этой программы может быть следующим:

Пример. Свойство глобальной инвариантности для программы вычисления биноминальных коэффициентов имеет вид

Те же самые обозначения можно использовать для локальной инвариантности по отношению к определенному месту

Пример. Условие, которое должно быть истинным, когда мы находимся в месте для программы подсчета вершин дерева выглядит следующим образом:

т.е. сумма вершин поддеревьев в стеке плюс значение счетчика С есть число вершин дерева X.

9.6.4. Взаимное исключение

Понятие критической секции и взаимного исключения было введено ранее. Вернемся к ним и сформулируем свойства корректности программ. Рассмотрим два параллельных процесса Предположим, что каждый процесс содержит секцию которая критична к попеременному выполнению команд из секции другого процесса. Например, это может быть доступ к распределяемому устройству (такому, как диск) или распределяемой переменной. Как уже говорилось, если природа этих секций такова, что они ни при каких обстоятельствах не могут выполняться одновременно, то их называют критическими.

Свойство взаимного исключения для С, и можно представить следующим образом:

Это свойство означает, что всегда, когда активно хотя бы одно место секции то в секции не может быть ни одного активного места, и наоборот.

9.6.5. Отсутствие дедлока

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

Рассмотрим набор ожидающих мест, V не все из которых терминальные. Пусть являются полными входными условиями, соответствующими этим местам. Чтобы предотвратить дедлок в требуется выполнение следующего свойства:

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

Для того чтобы предотвратить возможность дедлока во всей программе, необходимо налагать подобные требования на каждый набор ожидаюших мест, исключая

Пример. Условие отсутствия дедлока для программы вычисления биноминальных коэффициентов является следующим:

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