Конкретна форма та склад; EWSTПерекласти

Правильність у композиційних моделях

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

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

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

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

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

Справа незмінно і завжди

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

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

У світі часової логіки властивості завжди називають «інваріантами», тоді як інваріантні властивості називають «індуктивними інваріантами». З іншого боку, у світі послідовної перевірки програм інваріантні властивості називаються "інваріантами", і властивості завжди не мають назви. (Однак у методі В їх називають "твердженнями"). Це призвело до певної плутанини (див. Сторінку аксіоми заміщення).

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

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

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

Наші дослідження

У своєму дослідженні ми з Мані Ченді вирішили таку проблему: чи можемо ми знайти властивості компонентів, досить сильних для складання, але досить слабких, щоб зберегти абстракцію? Зокрема, ми зосереджуємось на двох формах композиції: екзистенціальній (екзистенційна властивість, що зберігається в системі, як тільки вона є хоча б одним компонентом), та універсальній (універсальна властивість, що зберігається в системі, як тільки вона є у всіх компоненти). Ми розглядаємо ці дві форми композиції в загальному контексті. Компоненти - це абстрактні сутності, не обов’язково програми. Він не повинен мати таких атрибутів, як "стани" або "обчислення". Вони складаються із закону композиції, який не повинен бути паралельним (зокрема, він не повинен бути симетричним чи ідемпотентним).

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