АЛГЕБРАЇЧНЕ ПРОЄКТУВАННЯ ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ

Анотація

Анотація. У статті розглянуто алгебраїчний підхід до проєктування та тестування програмного забезпечення. Метою статті є розробка класу, який реалізує арифметику Пеана. Арифметика Пеана є однією з базових конструкцій при аксіоматичному побудуванні математики. Клас арифметики, який представлений в статті є півгрупою натуральних чисел і є першим в ієрархії числових класів (група цілих чисел, кільце цілих чисел, поле раціональних чисел) для демонстрування небезпечності універсального поліморфізму підтипів та порушення принципу підстановки Лісков. Методи дослідження: під час дослідження використовуються базові положення методу проєктування по контракту Бертрана Меєра та методу формальної розробки RAISE, які дозволяють застосовувати формальну логіку. Наукова новина дослідження полягає в тому, що змінене трактування до функціонального типу методів класу та більш широке використання вимог до класу у вигляді алгебраїчних рівностей, якими описуються вимоги до інваріантів, передумов та післяумов. Об’єднання вимог до функціональних типів і цих рівностей логічною зв’язкою ‘і’ дозволяє однозначно прогнозувати порушення принципу підстановки та вимагає змінення правила підстановки (subsumption). Крім цього, звертається увага на властивість категоричності відповідної алгебраїчної моделі, яка робить неможливими некоректні реалізації, на прямі аналогії між аксіоматичним викладенням математичної теорії та розробкою технічного завдання програмістам. Також, даний підхід значно спрощує підбір тестів для димового тестування (smoke testing) програмного забезпечення. Висновки. Алгебраїчне проєктування та тестування базується на математичних принципах, що дозволяє: уникати двозначності і неоднозначності в описі функціональності; забезпечувати точність та однозначність у формулюванні вимог до програми; автоматизувати процес генерації тестових випадків та перевірки роботи, відповідно підвищувати надійність; виявляти і усувати помилки ще на стадії розробки та прискорювати розробку програмного забезпечення. Запропоновані в статті доповнення до алгебраїчного підходу проєктування по контракту та методу формальної розробки RAISE демонструють універсальність алгебраїчного проєктування, яке дозволяє перейти від мистецтва програмування та мистецтва тестування програм до формальних технологічних прийомів.