int ind1 = start, ind2 = finish; int temp; /// Введем три непересекающихся множества: /// S1: {tower1(i), start <= i =< ind1-1} /// S2: {tower1(i), ind1 <= i =< ind2} /// S1: {tower1(i), ind2+1 <= i =< finish} /// Введем следующие логические условия, /// играющие роль инвариантов циклов нашей программы: /// P1: объединение S1, S2, S3 = tower1 /// P2: (S1(i) < item) Для всех элементов S1 /// P3: (S3(i) >= item) Для всех элементов S3 /// P4: item - случайно выбранный элемент tower1 /// Нетрудно видеть, что все условия становятся /// истинными после завершения инициализатора цикла. /// Для пустых множеств S1 и S3 условия P2 и P3 /// считаются истинными по определению. /// Inv = P1 & P2 & P3 & P4 while (ind1 <=ind2) { while((ind1 <=ind2)&& (tower1[ind1] < item)) ind1++; //(Inv == true) & ~B1 (B1 - условие цикла while) while ((ind1 <=ind2)&&(tower1[ind2] >= item)) ind2--; //(Inv == true) & ~B2 (B2 - условие цикла while) |