9.8. Свойства предшествования

Третий класс рассматриваемых нами свойств составляют свойства, которые называются свойствами предшествования и выражаются с помощью оператора «до тех пор пока» и дополнительного оператора предшествования Р, который можно рассматривать как частный случай оператора . В простейшем случае свойства предшествования описываются следующим выражением:

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

Для дополнительного оператора предшествования Р выражение эквивалентно Выражение читается как предшествует и является истинным, если станет истинной в какой-либо ситуации, будучи до этого ложной, а ситуация, в которой стала истинной наступила ранее.

Несколько очевидных свойств дополнительного оператора предшествования Р можно получить из соответствующих свойств оператора и определения оператора Р:

Выражение 1 свидетельствует о том, что всегда предшествует себе, если является всегда ложной: не может предшествовать самой себе.

Выражение 2 означает транзитивность отношения предшествования: если предшествует а последняя предшествует то предшествует Выражение 3 дает индуктивную характеристику оператора Р. Оно говорит о том, что предшествует если в настоящей ситуации не истинно, истинно, либо в настоящей ситуации не истинно, а начиная со следующей ситуации предшествует

Выражение 4 говорит о том, что если никогда не становится истинной, то предшествует для любого

Выражение 5 характеризует линейность развития событий во времени для любых двух и или предшествует или предшествует или обе истинные в одной и той же ситуации.

Рассмотрим некоторые из свойств предшествования, использующих операторы и Р.

9.8.1. Безопасность

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

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

Другое свойство безопасности, использующее оператор является уточнением свойства

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

В отличие от этого свойства выражение (также относящееся к классу свойств безопасности)

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

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

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

9.8.2. Предусмотренная реакция (отзывчивость)

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

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

В большинстве практических случаев имеется дополнительная информация о и которая помогает сформулировать требования в более простой форме.

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

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

Это выражение означает, что если ресурс был предоставлен пользователю Л, то диспетчер не имеет права отнять его до тех пор, пока пользователь не присвоит ложное значение;

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

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

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

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

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

9.8.3. Справедливая отзывчивость

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

которое означает, что если предшествует то предшествует

Вместе с выражениями отзывчивости

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

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