Предыдущая страница реферата | 1  2  3  4  5 | Следующая страница реферата

означает .

Для цикла из примера 10.1, приведенному на рис. 11.3, инвариант выглядит так:

P: s=(Pk: 1£k0 обеспечивает проверку исходных данных на соответствие предусловию программы. Поэтому, после строки 5 мы можем быть уверены, что любое состояние, полученное в этой точке, будет удовлетворять предикату, написанному в виде комментария - {(nÎ N)Ù(n>0)}.

   Комментарий в конце 7 строки определяет состояния вычислительного процесса непосредственно перед входом в цикл. Комментарий после заголовка цикла (строка 8) - { s=Sk : 0 0) = ?

b then a:=a-b else

          if b