Методы и средства инженерии программного обеспечения
Модель формального доказательства конкретности программы - часть 3
(T[1: N] – массив целых) & (T '[1: N] – массив целых)
& ("i если i £ N (T [ i] = T [ i] )).
Доказательство очевидно, поскольку за семантикой оператора присваивания, обеспечивающая поэлементную пересылку чисел из Т в T’ , сами элементы при этом не изменяются и порядок их в Т і T' одинаковый. Получили, что условие (б) исходного утверждения выполнено. Первая строка доказанного утверждения совпадает с условием (а) исходного утверждения Аend и остается справедливой до конца работы алгоритма. В точке алгоритма с одной звездочкой выполняется оператор
(i < N) (T'( i)) > T' (i + 1) ® (T' ( i) и T' (i + 1) для изменения местами элементов.
В результате работы оператора будет справедливым такое утверждение:
$ i если i < N то (T'(i) < T'(i +1), которое является частью условия (в) утверждения Аend
(для одной конкретной пары смежных элементов массива T').
Очевидно, что семантика оператора обмена местами не нарушает условия (б) выходного утверждения Аend.
 |
i = 0
 |
|||
 |
|||
 |
Ø M = true
 |
