1.1 Специфікації програм

Розглянемо наступну конструкцію:, яка має назву «трійка Хоара», де - предикат передумови (стан програми на початку виконання), - програма, - предикат післяумови (стан програми при її завершенні). Ця конструкція представляє собою специфікацію програми [1].

Специфікація програми повинна точно описувати, що повинно бути отримано в результаті виконання програми.

«Трійка Хоара» [3] - це предикат, який приймає значення істина тоді і тільки тоді, коли програма почавшись у стані за скінчену кількість кроків закінчиться у стані.

Одним із способів специфікувати програму -- це виразити її у формі наказу використовуючи природну мову.

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

Предикат називається передумовою або вихідним твердженням; -- після умовою, обіцянкою або результуючим твердженням . Фігурні дужки { і } використовуються для того, щоб відокремити твердження від самої програми.

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

1.2 Перетворювач предикатів wp

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

Приклади:

1. Нехай S - команда присвоювання , а R - цe. Тоді,

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

2. Нехай S - це , а R - це . Виконання команди S завжди присвоює z значення , так як .

3. Нехай S - те ж саме, що і у прикладі 2, а R - це . Тоді , так як виконання S, що починається при , присвоює z значення у, а виконання S, що починається за , присвоює z значення х, яке не дорівнює у.

Для зазначення того, що виконання S, яке почалося у стані, що задовольняє предикату Q, закінчиться у стані, який задовольняє предикату R, будемо використовувати позначення .

Q називається передумовою, а R - післяумовою S. Подібно до цього називається найслабшою передумовою для S по відношенню до R, оскільки воно визначає множину всіх станів, таких, що виконання, яке почалося в будь-якому з них, закінчиться при істинному R.

Тобто позначення - це просто інша форма предикату .

Треба звернути увагу на те, що - в дійсності є реченням обчислювання предикатів, так як воно еквівалентно . Таким чином, в будь-якому стані воно або істинне, або хибне.

Зазвичай, команда S створюється з визначеною метою, а саме забезпечити істинність якої-небудь конкретної післяумови R.

- функція з двома аргументами: командою S і предикатом R. Якщо зафіксувати на деякий час довільну команду S, то можна записати як функцію одного аргументу . Функція перетворює будь-який предикат R в інший предикат . Це пояснює походження терміну «перетворювач предикатів» для .

Деякі властивості wp

Розглянемо предикат (для довільної команди S). Цей предикат описує множину станів, таких, що виконання S, яке почалося у будь-якому з цих станів, обов'язково закінчиться у стані, який задовольняє F. Але жоден з станів не може задовольняти F, так як F - це пуста множина. Отже, не може бути такого стану, для якого , і з цього отримуємо першу властивість.

Закон виключення дива:

. (1.2.1)

Дійсно, було б дивом, якби виконання могло завершитись в ніякому стані.

Другий закон такий: для будь-якої команди S і предикатів Q і R виконується наступна властивість.

Дистрибутивність кон'юнкції:

. (1.2.2)

Формула (1.2.2) є тавтологією. Це можна показати, якщо спочатку роздивитися довільний стан , який задовольняє лівій частнині (1.2.2). Виконання команди , яке почалося у стані , закінчиться при істинних і . Отже, буде також істинно, і знаходиться у . Це показує, що із лівої частини випливає права. Далі припустимо, що знаходиться у . Тоді виконання , яке почалося у стані , обов'язково закінчиться в деякому стані , що задовольняє . Будь-яке таке задовольняє і і , так що знаходиться у і у . Отже, з правої частини випливає ліва. Разом з попередньою імплікацією це спричиняє те, що вони еквівалентні.

Закони (1.12.1) і (1.2.2) було отримано, спираючись на неформальну інтерпретацію . Тепер (1.2.1) і (1.2.2) можна прийняти за вихідні аксіоми і використовувати так, як це робиться для інших аксіом і законів обчислення предикатів. За допомогою цих аксіом можна довести ще два корисних закони.

Закон монотонності:

якщо , то (1.2.3)

Дистрибутивність диз'юнкції:

. (1.2.4)

1.3 Команди skip, abort і композиція команд

Розглянемо в якості визначення команди саме визначення в термінах wp.

Команда skip. При виконанні цієї команди нічого не робиться (треба припустити, що протягом дуже короткого часу). Ця команда еквівалентна «порожньому» оператору у мовах програмування.

Визначення:

. (1.3.1)

Команда abort. Ця команда - єдина можлива команда, перетворювач предикатів якої є «постійною» функцією.

Визначення:

. (1.3.2)

Ця команда ніколи не буде виконуватися, оскільки вона може виконуватися тільки у стані, який задовольняє F, але жоден з станів не задовольняє предикату F. Якщо коли-небудь виконання програми доходить до місця, в якому повинна виконуватися команда abort, то зрозуміло, що програма (і її доведення) помилкова, і потрібне аварійне завершення.

Послідовне сполучення - це один із способів складання великих програмних сегментів з менших. Нехай та - дві команди. Тоді - нова команда. Щоб її виконати, потрібно спочатку виконати , а потім .

Визначення:

. (1.3.3)

Наприклад:

()

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

Таким чином, може мати як інтерпретацію, так і .

Оператор «;» використовується для з'єднання двох суміжних незалежних команд в єдину команду приблизно так як в природній мові для з'єднання незалежних речень [1].

Доведення коректності команди skip, abort

і послідовного сполучення «;»

Ідея доведення коректності команд полягає у встановленні того, чи відповідає визначення команди визначенню , а це можна зробити перевіришви аксіоми (1.2.1) і (1.2.2) для кожної з команд.

Доведення коректності команди skip:

1. Аксіома «Виключення дива»:

.

Доведення

.

2. Аксіома «Дистрибутивність кон'юнкції»:

.

Доведення

.

Доведення коректності команди abort:

1. Аксіома «Виключення дива»:

.

Доведення

.

2. Аксіома «Дистрибутивність кон'юнкції»:

.

Доведення

.

Доведення коректності команди послідовного сполучення «;»:

1. Аксіома «Виключення дива»:

.

Доведення

з (1.2.1)

2. Аксіома «Дистрибутивність кон'юнкції»:

.

Доведення

.

1.4 Команда присвоювання

1.4.1 Присвоювання простим змінним

Команда присвоювання виглядає наступним чином: , де х - проста змінна, е - вираз, типи х і е співпадають. Таку команду читають «х отримує значення е».

Правильно команда може виконуватися тільки у стані, в якому може бути розраховано значення е (наприклад, якщо не відбувається ділення на 0). Виконання складається з обчислення значення е і запису отриманного значення в комірку пам'яті з ім'ям х. В результаті (значення) х замінюється на (значення) е. Якщо показати таку підстановку синтаксично, отримаємо:

Визначення:

, (1.4.1)

де - предикат, який описує множину всіх станів, в яких може бути обчисленно значення е (тобто, де е визначене).

Так як вирази е не визначаються формально, також формально не буде визначено предикат . Проте він повинен виключати всі стани, в яких обчислення значення е може не дати результату (наприклад, при діленні на нуль або при виході індексу за область значень).

Часто взагалі випускають і записують:

, (1.4.2)

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

Приклади:

1. . Тобто, виконання ніколи не може зробити .

2. .

3. .

4. Нехай с ? константа. Тоді, . Це означає, що виконання обов'язкого завершиться і дасть значення с в х, якщо і тільки якщо значення виразу е перед виконанням присвоювання було с.

Виконання присвоювання може змінювати лише ту змінну, яка стоїть в його лівій частині.

1.4.2 Обмін місцями значень двох змінних

Послідовність присвоювань може бути використана для взаємної заміни (перестановки) значень змінних х і у. Це можна показати за допомогою наступних перетворень:

Подібні перетворення доволі складно читати і писати. Тому замість них використовують ескіз доведення, такий як наведено нижче:

або

В ескізі доведення (зліва) твердження стоять поміж кожними двома командами. Твердження є післяумовою для першої команди і передумовою для другої. Часто ескіз доведення читається від кінця до початку, оскільки передумова визначається післяумовою та командою. Можна також скорочувати таке доведення, як показано в цьому ж ескізі (справа).

1.4.3 Кратне присвоювання простим змінним

Кратне присвоювання простим змінним має вигляд:

програмування команда вибір повторення

,

де - різноманітні прості змінні, - вирази. Для спрощення присвоювання скорочується до .

Команда кратного присвоювання виконується наступним чином. Спочатку обчислюються всі вирази. Нехай вони дали значення . Далі присвоюється , , ..., саме в такому порядку.

Кратні присвоювання корисні, оскільки вони легко описують зміни стану, які відбуваються більш ніж для однієї змінної. Їх формальне визначення - розширене визначення присвоювання для однієї змінної.

Визначення:

, (1.4.3)

де - описує множину станів, в яких можуть бути обчислені значення всіх виразів з вектору :

.

Приклади:

1. Присвоювання можна використовувати для обміну значень х і у.

2. Присвоювання здійснює «циклічне переставлення» значень х, у і z.

3.

.

1.4.4 Присвоювання елементу масиву

З функціональної точки зору на масиви, масив b являє собою просту змінну, яка містить в покажчику значення-функцію, а звичайна «індексація елементу масива» є просто використанням функції, яка знаходиться в даний момент в b, відносно аргументу і. Через позначається функція, яка відрізняється від b лише тим, що при аргументі і вона приймає значення е.

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

Визначення:

, (1.4.4)

де

позначає, що значення і знаходиться в області значень індексів масиву b (тобто, є правильним індексом для b).

Приклад:

(за визначенням)

(підстановка)

Отже, виконання завжди присвоює значення 5.

Доведення коректності команди присвоювання

1. Аксіома «Виключення дива»:

.

Доведення

.

2. Аксіома «Дистрибутивність кон'юнкції»:

.

Доведення

.

1.5 Команда вибору

Системи понять мов програмування зазвичай включають умовну команду, або оператор if, який дозволяє варіювати виконання своїх команд в залежності від теперішнього стану програмних змінних.

Наприклад, така команда може мати вигляд:

.

Виконання цієї команди записує в z абсолютну величину х: якщо , то виконується перша альтернатива , в іншому випадку виконується друга альтернатива . Цю команду також можна записати у наступному вигляді:

(1.5.1)

або ж, так як вона достатньо коротка і проста, в один рядок:

.

У команді (1.5.1) містяться дві складові виду (розділені символом ), де - логічний вираз, а - команда. Команда називається охороняємою командою, так як служить охороною входу , забезпечуючи те, що буде виконуватися тільки при виконанні умови .

Загальний вид команди вибору:

… (1.5.2)

де і всі - охороняємі команди. Кожне з може бути довільною командою - skip, abort, послідовним сполученням команд, присвоюванням, іншою командою вибору та ін.

Для скорочення запису загальний вид команди (1.5.2) будемо позначати через , а через будемо позначати диз'юнкцію .

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

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

Визначення:

(1.5.3)

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

Визначення:

(1.5.4)

Теорема про команду вибору

Доволі часто потрібна не найслабша передумова команди вибору, а лише перевірка того, чи спричиняє її відома передумова. В таких випадках корисна наступна теорема.

Теорема. Розглянемо команду . Нехай предикат задовольняє умовам

1)

2) для всіх і, .

Тоді (і тільки тоді)

.

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

(імплікація)

(закон де Моргана)

( не залежить від і)

(імплікація, двічі)

Тобто, маємо

(умови 1 і 2)

(з наведеного вище)

(з (1.4.4))

Отже, кон'юнкція припущень еквівалентна висновку, теорема доведена.

1.6 Команда повторення

1.6.1 Звичайний цикл «поки» і команда повторення

Цикл типу «поки» може мати, наприклад, такий вигляд:

.

Частіше такі цикли описують за допомогою блок-схем

Позначимо цикли типу «поки» так

,

де - охороняєма команда. Цей запис можна узагальнити до наступного, який будемо називати командою повторення і позначимо :

… (1.6.1)

де і кожна з - охороняєма команда.

Якщо описати роботу (1.6.1) одним реченням, то отримаємо: повторюйте (або ітеруйте) наступну дію: обирайте охорону , яка істинна, і виконуйте відповідну команду .

Після завершення всі охорони хибні. Вибір істинної охорони і виконання відповідної команди називають виконанням кроку циклу.

Допускається недетермінізм, тобто якщо істинні дві або більше охорони, обирається будь-яка з них (але тільки одна) і виконується відповідна команда. Така ситуація може виникнути на будь-якому кроці. Звідси видно, що еквівалентна:

…

де позначає диз'юнкцію охорон , або ж

,

де позначає команду вибору з тими ж самими командами, що охороняються, як і в (1.6.1).

Це означає, що, якщо всі охорони хибні, тобто якщо хибне, виконання циклу завершується. В іншому випадку виконується відповідна команда вибору , і процес повторюється. Одна ітерація циклу еквівалентна встановленню, що істинно, і виконанню .

1.6.2 Формальне визначення DO

Наступний предикат визначає множину станів, в яких виконання завершиться за 0 кроків через те, що всі охорони з самого початку будуть хибними, причому після завершення істинне:

.

Напишемо предикат при , який виражає множину всіх станів, в яких виконання закінчиться за або менше кроків при істинному . Визначення буде рекурсивним. Предикат буде визначатися через . Перший випадок, коли завершується через 0 кроків, - це той випадок, коли істинно . В іншому випадку відбувається хоча б один крок. Таким чином, повинно бути істинним на початку, і крок полягає у виконанні відповідної команди . Таке виконання завершується у стані, в якому до завершення циклу залишаеться або менше кроків. Подібний розгляд приводять до виразу

для .

Якщо згадати, що повинно відображати множину станів, в яких виконання завершується за кінцеву кількість кроків і за істинним , тобто з самого початку в кожному з таких станів повинно бути таке , що виконання циклу потребує не більше кроків, отримаємо:

Визначення:

(1.6.2)

1.6.3 Теорема про цикл, його інваріант і обмежуючу функцію

Теорема. Розглянемо цикл . Припустимо, що предикат Р задовольняє умові

1. для усіх і, .

Далі, нехай цілочислова функція задовольняє наступним умовам, де новий ідентифікатор:

2.

3. при

Тоді,

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

1.6.4 Анотування циклу і розуміння анотацій

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

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

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

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

(1.6.3)

…

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

1. Покажіть, що істинне перед початком виконання циклу.

2. Покажіть, що за всіма , тобто що виконання кожної команди, що охороняється, завершиться при істинному . Звідси випливає, що є інваріантом циклу.

3. Покажіть, що, тобто те, що в момент завершення виконання є істинним бажаний результат.

4. Покажіть, що, тобто, що обмежена знизу, доки цикл не завершиться.

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

1.7 Побудова програм

Програма називається правильною по відношенню до заданої післяумови та передумови , якщо має місце .

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

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

Принцип 1. Програма і її доведення повинні будуватися одночасно.

Принцип 2. Використовуйте теорію для проникнення у суть роботи; застосовуйте інтуіцію і здоровий глузд там, де це можливо, але одразу повертайтеся до пітримки з боку формальної теорії, коли виникають складнощі.

Принцип 3. Вивчіть властивості об'єктів з якими повинна працювати програма.

Принцип 4. Ніколи не нехтуйте будь-яким з фундаментальних принципів як очевидним, оскільки тільки усвідомлене використання таких принципів може сприяти успіху.

1.8 Програмування як цілеспрямована діяльність

Принцип 5. Програмування - цілеспрямована діяльність.

Принцип 6. Перед тим як пробувати вирішити задачу, треба впевнитися, що ви розумієте, в чому вона складається.

При програмуванні цей загальний принцип перетворюється у наступний.

Принцип 7. Перед тим як будувати програму, уточніть і роз'ясніть для себе передумову і післяумову.

1.8.1 Стратегія побудови команди вибору

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

Принцип 8. Між інших рівних умов робіть охорони у командах вибору настільки сильними, наскільки це можливо, для того щоб деякі помилки призводили до аварійних зупинок програми.

1.8.2 Стратегія побудови команди циклу

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

У термінах високого рівня наведену стратегію можна відобразити наступним чином:

Принцип 9. Між інших рівних умов робіть охорону циклу настільки слабкою, наскільки це можливо, для того щоб помилка могла викликати зациклення.

1.9 Теоретичні аспекти «Програмування за контрактом»

В більшості об'єктно-орієнтовних мов програмування не приділяється багато уваги семантичним властивостям класу. Кожен клас має список своїх операцій. Але інформація про те, коли можна викликати той чи інший метод, які параметри не обов'язкові, що треба очікувати в результаті виконання, не є формальною. Більшість такої інформації або відсутня або міститься у вигляді коментарів. В цьому випадку ми отримаємо дублювання інформації, оскільки реалізація методу має відповідати коментарям або іншій документації, і відсутність можливості контролювати поведінку під час виконання коду. Для усунення цих недоліків розроблено формальний спосіб, що визначає відносини між класами та їх клієнтами (тобто кодом, що створює екземпляри цих класів і взаємодіє з ними), який недвозначно встановлює права та обов'язки сторін, що отримав назву "проектування за контрактом".

Проектування за контрактом (Design by Contract) - це встановлення відносин між класом і його клієнтом у вигляді формальної домовленості, які однозначно визначають права та обов'язки обох сторін. Тільки через точне визначення вимог та відповідальності для кожного модуля можна сподіватись на досягнення значного ступеня довіри до великих програмних систем[2].

1.9.1 Коректність ПЗ

Будь-яка функція не є ні коректною, ні некоректною. Поняття коректності набуває сенсу тільки в контексті очікуваного результату. Функція може бути коректною по відношенню до якогось певного висловлювання, і бути хибною по відношенню до іншого. В цьому випадку сигнатура методу не несе достатньо інформації для визначення того, є метод коректним чи ні. Семантика методу передається його назвою (хоча ім'я методу Remove ніяк не може говорити про поведінку цього методу для порожній колекції) або коментарями. Але коментарі часто застарівають, семантика методів змінюється таким чином, що ім'я перестає відображати суть методу, але головне, що це явно не той шлях, який зможе забезпечити надійність розроблюваного ПЗ.

Поняття коректності ПЗ можна розглядати тільки по відношенню до деякої специфікації, в той час, як програмний елемент сам по собі не може бути ні коректним, ні некоректним [2].

1.9.2 Формула коректності. Сильні та слабкі умови

Нехай A - це деяка операція, тоді формула коректності (correctness formula) - це вираз вигляду:

Формула коректності, звана також тріадою Хоара, говорить наступне: будь-виконання А, що починається в стані, де Q істинне, обов'язково завершиться і в заключному стані буде істинним R, де Q і R - це твердження, при цьому Q є передумовою, а R - післяумовою [2].

Наведена вище формула коректності визначає повну коректність (total correctness), яка гарантує скінченність операції A. Крім цього існує поняття часткової коректності (partial correctness), яке гарантує виконання післяумови R тільки за умови завершення виконання операції A.

Розглянемо наступну тріаду Хоара:

Ця тріада коректна, тому що якщо перед виконанням операції передумова виконується і значення x дорівнює 5, то після виконання цієї операції післяумовою (x більше нуля) буде гарантовано виконуватися (за умови коректної реалізації цілочислової арифметики). З цього прикладу видно, що наведена післяумова не є найсильнішою. Найсильнішою післяумовою при заданій передумові є , а найслабшою передумовою при заданій післяумові є . З виконуваної формули коректності завжди можна отримати нові виконувані формули, шляхом послаблення післяумови або посилення передумови.

1.9.3 Твердження

Специфікація і реалізація нерозривно пов'язані один з одним: специфікація говорить про те, що повинна робити система, а реалізація визначає, як це буде досягнуто. Обидва ці аспекти програмного продукту повинні розвиватися одночасно, чого в більшості програмних проектів не відбувається. (Хоча, насправді, далеко не у всіх проектах специфікація взагалі існує в будь-якому формальному вигляді, в такому випадку єдиним джерелом специфікації є вихідний код, що в свою чергу робить неможливим перевірити його коректність.) Якщо специфікація і реалізація знаходяться в різних джерелах, ми стикаємося з класичною проблемою дублювання інформації, і в цьому випадку неузгодженість цієї інформації є всього лише питанням часу. У проектуванні за контрактом вираз специфікації здійснюється за допомогою механізму тверджень (assertions).

Твердження - це логічний вираз, яке має бути істинним на деякій ділянці програми і може включати сутності нашого ПЗ. Твердженнями можуть служити звичайні булеві вирази з деякими розширеннями. Так, у твердженнях крім булевих виразів можуть застосовуватися функції (але з деякими обмеженнями: це повинні бути функції без «побічних ефектів», тобто не змінюють стан об'єкта). А для післяумови необхідна можливість звернутися до результату виконання функції, а також до значення, яке було до початку виконання цієї функції.

1.9.4 Передумови та післяумови

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

Нехай передумова визначається ключовим словом «require», а післяумова - ключовим словом «ensure». Тоді, якщо з деякою функцією r пов'язані затвердження «require pre» і «ensure post», то клас говорить своїм клієнтам наступне [2] :

«Якщо ви обіцяєте викликати R в стані, що задовольняє «pre», то я обіцяю в заключному стані виконати «post»».

Передумовою та післяумовою визначають контракт між двома програмними елементами: класами-клієнтами та класами-постачальниками, а будь-який хороший контракт встановлює чіткі зобов'язання між його учасниками. Зобов'язання одного учасника визначають вигоди іншого і навпаки. Це вірно як для контрактів між людьми (або людьми і компаніями), так і для контрактів між програмними елементами.

Передумова зв'язує викликаючий код: визначаються умови, за яких виклик методу клієнтом легітимний (наприклад, x> 0 для функції Sqrt або Count! = 0 для функції Pop класу Stack). При цьому зобов'язання клієнта приносять вигоду класу-постачальнику, оскільки класу, що виконує операцію, не потрібно турбуватись про те, що робити при порушенні передумови: повертати значення за замовчуванням або код помилки, генерувати виключення, зберігати інформацію про помилку в потік вводу-виводу або переривати виконання програми.

1.9.5 Інваріанти класу

Передумови і післяумови характеризують конкретні функції, але не клас в цілому. Екземпляри класу часто мають деякі глобальні властивостями, які повинні виконуватися після створення об'єкта і не порушуватися протягом усього часу життя. Такі властивості носять назву інваріантів класу (class invariants). Вони визначають більш глибокі семантичні властивості та обмеження, властиві об'єктам цього класу.

Такими властивостями можуть служити внутрішні умови (деякий поле не дорівнює null або кількість елементів невід'ємне) або правила узгодженості внутрішнього стану об'єкта. Кожна така умова не пов'язує конкретні функції, а характеризує об'єкт в кожен момент часу.

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

Затвердження Inv є коректним інваріантом класу, якщо і тільки якщо воно задовольняє наступним двом умовам [2]:

1. Кожен конструктор, який можна застосовувати до аргументів, що задовольняє його передумов в стані, в якому атрибути мають значення, встановлені за замовчуванням, виробляє заключне стан, що гарантує виконання Inv.

2. Кожен відкритий метод класу, що викликається з аргументами в стані, що задовольняє Inv і передумов, виробляє заключне стан, що гарантує виконання Inv.

1.9.6 Твердження та перевірка вхідних даних

Проектування за контрактом призначено для формалізації взаємини двох програмних елементів всередині довіреної середовища і не призначене для взаємодії програмного елемента із зовнішнім світом. Головний принцип захищеного коду «все вхідні дані хибні, поки не доведено протилежне» [8] залишається в силі, і про нього не слід забувати при розробці будь-яких додатків, незалежно від того, побудовані вони за принципами проектування за контрактом або без нього.

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

1.9.7 Проектування за контрактом та захисне програмування

Одним з головних принципів проектування за контрактом є відсутність перевірок передумов всередині тіла програми. Це правило суперечить принципам захисного програмування, в якому «відкриті методи класу припускають, що дані небезпечні і відповідають за їх перевірку і виправлення. Якщо дані були перевірені відкритими методами класу, закриті методи можуть вважати, що дані безпечні »[9]. При цьому усередині відкритих методів рекомендується застосовувати обробники помилок (наприклад, генерувати виключення або повертати відповідний код помилки у разі невірних вхідних даних), а в закритих методах застосовувати затвердження (assertions) (оскільки це характеризує програмні помилки).

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

Крім того, в захисному програмуванні існує негласне правило, за яким «зайва перевірка ніколи не зашкодить», і дійсно, якщо розглянути простий приклад (наприклад, функцію вилучення квадратного кореня double Sqrt (double x)) може здатися, що жодної шкоди від додаткової перевірки немає і бути не може, але чи так це насправді?

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