Розширення області значення змінної

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

Як приклад розберемо класичну задачу «Шахрай на на соціальній допомозі». В оригінальному варіанті розглядаються три потенційно нескінченних упорядкованих за алфавітом списку прізвищ - співробітники дослідницького центру IBM, студенти Колумбійського університету та безробітні Нью-Йорка. Потрібно знайти перше з прізвищ, що зустрічається у всіх трьох списках (у припущенні, що воно є).

Задача 2.5. Знайдіть мінімальне число, що міститься в кожному з двох упорядкованих за зростанням масивів цілих чисел, в продовженні, що таке існує.

Розв'язання. Нехай наявні масиви - це a, і . Змінні, що містять значення індексів для кожного з цих масивів, позначимо черезi, і відповідно, а індекси шуканого числа в кожному з них , і .

Якщо не включати в передумова інформацію про те, що масиви є впорядкованими (не забуваючи про це, звичайно), то перед- і постумови шуканої програми буду мати вигляд , і .

Розширення області значень змінних i, j і k природний спосіб побудови інваріанта в даному випадку: . В якості обмежуючій функції можна взяти , вибір початкових присвоювань S0 проблем теж не викликає - ясно, що оператори ; ; ;" зроблять інваріант істинним.

В якості дій, які будуть наближати цикл до завершення можна використовувати оператори "i ++;", "j ++;" і "k ++;". При цьому зрозуміло, що кожен з них зобов'язаний бути присутнім у підсумковій програмі.

Обчислимо wp ("i ++;", I) = (i + 1≤iv). Це означає, що збільшення індексу i в циклі потрібно робити, коли . На жаль, записати подібне умова в програмі неможливо, так як змінної в ній просто може не бути!

Легко помітити, однак, що виконання умови при істинному інваріанті I означає, що число a[i] менше шуканого в задачі, а це може бути тільки за умови істинності диз'юнкції . Аналогічно укладаємо, що якщо істинна диз'юнкція , то можна збільшувати значення індексу j, а при істинності предиката - індексу .

Це вже дозволяє написати програму, але якщо уважно дослідити доказ її правильності, то можна виявити можливість для її спрощення, що і реалізовано нижче.

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

public class Arr3 {public static void main(String[] args){ int a[] = { 1, 2, 4, 8,16,32,64,128};int b[] = {10,12,14,16,18,20,22, 24};int c[] = { 9,12,13,16,17,20,21, 24};inti = 0, j = 0, k = 0;while (true) { if (a[i] < b[j]) {i++; continue; }if (b[j] < c[k]) {j++; continue; }if (c[k] < a[i]) {k++; continue;}Xterm.println("Минимальное общее число=" + a[i]);return; } }}

Обов'язково перевірте всі п'ять умов правильності цієї підсумкової програми.

Завдання для самостійного рішення

При вирішенні завдань необхідно побудувати і довести правильність побудованої програми виду "S0; while (e) S;", а за відсутності в умові задачі явно заданих інваріанта циклу і обмежуючій функції пояснити попередньо, яким чином вони були отримані.

Задача 1.1. Напишіть програму, що друкує n-е число Фібоначчі . При написанні програми використовуйте Число в програмі змінити не можна.

Задача 1.2. Напишіть програму, що знаходить приватна і залишок від ділення на , не використовуйте операції множення і ділення. При написанні програми покладіть , , . Величини x і у в програмі змінювати не дозволяється.

Задача 1.3. Напишіть програму, що знаходить найбільший спільний дільник gcd (X, Y) двох цілих позитивних чисел X і Y, не використовує операцій множення і ділення і не змінну величин X і Y. При написанні програми покладіть ,

Вказівка. Скористайтеся наступними властивостями найбільшого загального дільника двох чисел, що не рівних одночасно нулю (не забудьте навчитися доводити всі ці властивості):

,

,

.

Задача 1.4. Напишіть програму, що знаходить наближене значення квадратного кореня із заданого невід’ємного цілого числа n. Ось більш точне формулювання перед- і постумови: При написанні програми величину n змінювати не можна. Для побудови інваріанта видаліть з постумови кон'юнктивний член . Оцініть тимчасову складність отриманої програми і порівняйте її зі складністю програми, побудованої в задачі 2.1.

Задача 1.5. Напишіть програму, що визначає перше входження заданого цілого числа х в заданий масив масивів цілих чисел . Значення елементів масиву b і числа х, m і n в програмі змінювати не можна. У момент завершення має бути або , або, якщо числа x в масиві немає, . Точні перед- і постумови необхідної програми такі: , .

ВКАЗІВКА. Використовуйте інваріант, який стверджує, що х не перебуває у вже перевірених рядках і серед вже перевірених елементів поточного рядка I В якості обмежуючій функції візьміть

Задача 1.6. Напишіть програму (бінарний або двійковий пошук), визначальну для впорядкованого за не зменшенням масиву цілих чисел і заданого цілого числа х позицію , в яку може бути вставлене це число без порушення впорядкованості масиву. Точні перед- i постумови необхідної програми, тимчасова складність якої не повинна перевершувати , такі; . При написанні програми величини х, n і елементи масиву b зраджувати не дозволяється, для побудови інваріанта використовуйте метод заміни константи змінної.

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

Лекція 11.