Искусственный интеллект

Пример. Для программы вычисления биноминальных коэффициентов имеем N (0 < к < п) г> {[(в_месте (/и4) ^> (у2* 0) л (уу mod у2 - G) л (п-к < у{ S п)] л л (0 < у2 < к) U (в_месте (lt) л вместе (те) /\уг= С* ]}. Это свойство говорит о том, что до тех пор, пока не будет достигнуто окончание программы с правильным результатом, должны выполняться свойства чистого поведения и глобальной инвариантности. 210 9.8. Свойства предшествования 9.8.2. Предусмотренная реакция (отзывчивость) Свойства, выражаемые формулой w, => 0w2, относятся к числу свойств отзывчивости, выполнение которых гарантирует, что на каждую ситуацию, в которой формула w, истинна, программа отвечает в конце концов истинным значением формулы w2. Часто желательно дополнить это свойство требованием, чтобы формула w2 никогда не становилась истинной, если этому не предшествует истинность формулы и>р т.е. чтобы программа не реагировала на непредусмотренную ситуацию. Это свойство в общем случае можно выразить с помощью оператора предшествования, но в каждом конкретном случае требуется тщательно выбирать ситуации, после наступления которых проверяется предшествование. Хорошим примером выражения, задающего свойство предусмотренной отзывчивости, является следующее: