Усунення кон'юнктивного члена

Цей метод гарний тим, що взявши за умову продовження циклу усунений кон'юнктивний член, ми автоматично добиваємося істинності четвертого пункту теореми 10.1, яка гарантує правильність побудованого циклу.

Розглянемо як приклад наступну задачу.

ЗАВДАННЯ 10.1. Напишіть програму, яка знаходить наближене значення квадратного кореня а із заданого невід'ємного цілого числа . Ось більш точне формулювання перед- і постумови: При написанні програми величину змінювати не можна.

Рішення. Побудуємо інваріант за допомогою методу усунення кон'юнктивного члена з післяумови .

Умовою продовження циклу e може бути заперечення видаленого кон'юнктивного члена: , що еквівалентно вибору обмежуючої функції . Істинність інваріанта перед початком виконання циклу легко встановлюється присвоюванням "a = 0;" і нам залишається тільки зрозуміти, як реалізувати тіло циклу .

Для того щоб цикл завершився, величина а повинна збільшуватися. Найпростіший спосіб - збільшувати а на одиницю на кожній ітерації циклу. Легко помітити, що це перетворення зберігає інваріант, тому побудову програми завершено. Перший варіант програми буде строго відповідати її специфікації.

Текст програми.
public class Sqrt {
public static void main (String [] args) throws Exception {
int n = Xterm.inputInt ("n ->");
int a = 0;
while (n> = (a +1) * (a +1))
a + = 1;
Xterm.println ("sqrt (" + n + ") =" + a);
}
}
Цю програму можна переписати в трохи більш компактному вигляді:

Фрагмент програми

 

int a, n = Xterm.inputInt ("n ->");
for (a = 0; n> = (a +1) * (a +1); a + +);
Xterm.println ("sqrt (" + n + ") =" + a);

Доведемо всі п'ять умов її правильності.

 

1)

 

2) ,

Тому .
Отриманий предикат завідомо правдивий, якщо помилкові або , у протилежному випадку він легко спрощується:

.

Істинність першого кон'юнктивній члена випливає з припущення про істинність , а істинність другого - з істинності .

3) .

4).

5) , , в припущенні, що правдиві й (тому що з істинності випливає .
Отже .

 

Застосуємо метод усунення кон'юктивного члена для побудови інваріанта циклу при вирішенні ще одного завдання.

ЗАВДАННЯ 10.2. Напишіть програму (лінійний пошук), яка визначає перше входження заданого цілого числа x в заданий масив цілих чисел . Відомо, що знаходиться в масиві b. Значення елементів масиву b і число x в програмі змінювати не можна.

 

Рішення. Випишемо формально задані нам перед- і післяумови:

.

 

Враховуючи те, що домогтися істинності третього кон'юнктивного члена одним або кількома простими присвоювання важко, усунемо саме його. Тоді отримаємо . Умовою продовження циклу можна взяти заперечення видаленого члена , а інваріант легко зробити істинним, виконуючи команду "i = 0;", тому програма повинна мати вигляд "i = 0; while (x! = b [i]) S; " з невідомим нам поки S.

Обмежуючою функцією можна спробувати взяти , a для того, щоб вона зменшувалася, досить збільшувати на кожній ітерації циклу.

Зрозуміло, що збільшуючи і більше, ніж на одиницю, можна пропустити перше входження в масив, тому однією з команд, що входять в S, повинна бути команда "i = i +1;". Так як виконання даної команди за умови істинності зберігає інваріант, то ця команда є єдиною в тілі циклу. Програма побудована.

Текст програми.
public class SearchL {
static int b [], x;
public static void main (String [] args) throws Exception {
int m = Xterm.inputInt ("m ->");
b = new int [m];
for (int k = 0; k <m; k + +)
b [k] = Xterm.inputInt ("b [" + k + "] ->");
x = Xterm.inputInt ("x ->");
int i = 0;
while (x! = b [i])
i + = 1;
Xterm.println ("i =" + i);
}
}

Доведемо правильність цієї програми.

1) wp (S0, I) = wp("i = 0;",

, що випливає з .

2) wp(S,I)=wp(

"i + = 1;"

, тому

.

Дана імплікація є тавтологією, бо якщо в під масиві елемент не зустрівся, то з умови задачі випливає, що елемент з індексом в масиві завідомо є (тобто I + 1 < m).

3).

4).

5) wp("h1 = h; S;",h<h1)=wp("h1 = m-i;",wp "i + = 1;", m - i<h1))=wp("h1 = m-i;",m-i-1<h1)=(m-i-1<m-i)=T.
Отже (I∧e⇒wp("h1 = h;

S;"., h<h1))=(I∧e⇒T)=(!I⋁!e⋁T)=T

10.4. Заміна константи змінною

Як перший приклад використання цього методу побудови інваріанта розглянемо просту задачу сумовування елементів масиву.

Задача 2.3. Напишіть програму, що знаходить суму s елементів заданого цілочисельного масиву , елементи якого і величину n змінювати не можна. Точні перед- і пост умови:

Розв'язання. У післяумову входить константа , яку ми можемо замінити новою змінною i, що змінюється в діапазоні від 0 до включно. Таким чином, метод заміни константи змінною приводить нас до інваріанта. Зрозуміло, що в якості обмежуючої функції слід взяти .

Істинності інваріанта легко домогтися обнуленням величин і s, тому шукана програма буде мати вигляд "i = 0; s = 0; while (i <n) S;" з невідомим нам поки тілом циклу S.

Для того, щоб цикл завершився, необхідно зменшувати h, що цілком природно робити, збільшуючи i на одиницю на кожній ітерації циклу. Використовуючи інваріант, знаходимо, що другим необхідною дією є додавання до s значення b[i]:

Текст програми.

public class SumArr {staticint b[];public static void main(String[] args) throws Exception { int n = Xterm.inputInt("n -> ");b = new int[n]; for (int k=0; k<n; k++)b[k] = Xterm.inputInt("b["+k+"] -> ");inti=0, s=0;while (i< n) { s += b[i]; i += 1; }Xterm.println("s = " + s); }}

Доведемо її правильність.

1) Враховуючи, що wp("i=0;s=0;",

,

то .

2)

 

.

Тепер обчислимо.

Даний предикат свідомо істинний, якщо правдивий один з перших чотирьох його диз'юнктивних членів. В іншому випадку маємо і , тому правдивий п'ятий його диз'юнктивний член, отже предикат є тавтологією.

3).

Очевидно, що .

.

5)

Отже

Побудуємо більш швидку програму знаходження наближеного значення квадратного кореня.

Задача 2.4. Напишіть програму, що знаходить наближене значення квадратного кореня із заданого невід'ємного числа n. Точні перед- і постумови необхідної програми, тимчасова складність якої не повинна перевершувати такі: При написанні програми величину n змінювати не можна.

Розв'язання. Побудуємо інваріант за допомогою методу заміни константи на змінну b. З умови задачі випливає, що , отже інваріантом є предикат . Умова продовження циклу легко виходить з того факту, що предикат повинен бути тавтологією , а це означає використання обмежуючій функції .

Після присвоювань "a = 0; b = n + 1;" предикат 𝐼 стає істинним, отже наша програма має вигляд "a = 0; b = n + 1; while (a + 1! = b) S;" з невідомих поки тілом циклу S.

Для того щоб цикл завершився, необхідно зменшуватись h, що еквівалентно зближенню чисел 𝑎 і 𝑏. Зменшення різниці 𝑏-𝑎 на одиницю на кожній ітерації циклу не дозволить досягти необхідної b умові задачі ефективності програми. Потрібна тимчасова складність може бути отримана при використанні методу ділення відрізка [a, b] навпіл на кожній ітерації і виборі тієї з половинок, на якій лежить шукане наближене значення квадратного кореня. Реалізація даної ідеї призводить до наступній програмі.

Текст програми.

publicclassSqrt3 {public static void main(String[] args) throws Exception {int a, b, n; n = Xterm.inputInt("n -> "); a = 0; b = n+1;while (a+1!= b) {int c = (a+b)/2;if (c*c <= n) a = c;else b = c; } Xterm.println("sqrt(" + n + ") = " + a);}}

Доведіть самостійно її правильність та оцініть ефективність.