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

9.6. Инвариантные свойства Программные свойства, которые всегда должны выполняться для данной программы, называют инвариантными свойствами. Они описываются формулой вида N Dw. Это означает, что формула w должна быть истинна для каждой последовательности допустимого вычисления, определяемого начальными условиями этой формулы, т.е. w — инвариант по отношению к такому допустимому вычислению (исходя из этого, можно было бы вместо N Ow написать N w). Чтобы подчеркнуть тот факт, что мы имеем дело с предусловием 1,(х, у, п), иногда будем записывать ?(ж, у, п) z> Ow. Формула в этом виде выражает инвариантное свойство, известное как свойство безопасности, базирующееся на предположении, что ничего плохого случиться не может, если выполнены начальные предпосылки ?(*, у, п). Чаще всего полное предусловие ^(дс, у, п) при формулировке того или иного свойства будем оговаривать отдельно, записывая перед формулой свойства, его часть или вообще ничего не записывая.