К. М. Лавріщева програмна інженерія підручник Київ, 2008
 Скачать 5.23 Mb.
|
|
Список літератури до розділу 5 1. Demark D.A., McGowan R.L. SADT: Structured Analysis and Design Technique. New York: McCray Hill, 1988 .– 378 c. Розділ 5 143 2. Skidmore S., Mills G. Farmer R. SSADM: Models and Mehtods. – Prentice–Hall, Englewood Cliffs, 1996.–581с. 3. Марка Д.А., МакГруэн К. Методология структурного анализа и проектирования. – М.: МетаТехнология, 1997.– 346 с. 4. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на C++, 2–е изд. – М.: Изд–во Бином, 1998. – 560 с. 5. Гамма Э., Хелм Р., Джонсон Р., Влиссидес Дж. Приемы объектно- ориентированного проектирования. Паттерны проектирования. – СПб: Питер, 2001. – 368 с. 6. The Unified Modeling Language (UML) Specification. – 1.3. UML Specification, revised by the OMG. – July 1999. – 620 p. 7. Рамбо Дж., Джекобсон А , Буч Г. UML. Специальный справочник.– СПб.: Питер .– 2002. – 656 с. 8. Сrnkovik I, Larsson S., Stafford J. Component–Based Software Engineering: building systems from Components at 9 th Conference and Workshops on Engineering of Computer-Based Systems.– Software Engineering Notes. – 2002.– 27.– N 3 .– Р. 47–50. 9. Gamma E., Helm R., Johnson R., and Vlissides J. Design Patterns, Elements of Reusable Object–oriented Software, – N.-Y.: Addison–Wesley, 1995. – 345 p. 10. Грищенко В.Н., Лаврищева Е.М. Методы и средства компонентного программирования // Кибернетика и системный анализ, 2003. – №1. – С. 39– 55. 11. Лаврищева Е.М. Методы программирования. Теория, инженерия, практика. Киев: Наукова думка, 2006.–451с. 12. Weide B., Ogden W., Sweden S. Reusable Software Components / Advances in Computers, 33. – Academic Press, 1991. – P. 1–65. 13. Jacobson I., Griss M., Johnson P. Software Reuse: Architecture, Process and organization for Business Success – Addison Wesley, Reading , MA, May 1997. – 501 p. 14. Эммерих В. Конструирование распределенных объектов. Методы и средства программирования интероперабельных объектов в архитектурах OMG/CORBA, Microsoft COM и Java RMI. – М.: Мир, 2002. – 510 с. 15. Kiselev. I. Aspect–Oriented Programming with AspectJ. Indianapolis, IN, USA: SAMS Publishing, 2002. – 164 p. 16. Павлов В. Аспектно-ориентированное программирование //Технология клиент-сервер, № 3–4. – С. 3–45. 17. Чернецки К., Айзенекер У. Порождающее программирование. Методы, инструменты, применение.– Издательский дом Питер. – М.: СПб. – Харьков. – Минск, 2005. – 730 с. 18. Yang J. Web Services Componentization//Ibid.–P.35–40. 19. Плескач В.Л., Рогушина Ю.В. Агентные технологии.–К.: КНТЕУ, 2005.– 337с. 20. Shoham. Y. Agent–oriented programming. – Artif.Intell. – 1993–60, №1. – P. 51– 92. 21. Трахтенгерц Э.А. Взаимодействие агентов в многоагентных средах // Автоматика и телемеханика. – М.: Наука. – 1998. – 8. – С. 3–52. 144 Розділ 5 22. Дрейган Р. Будущее программных агентов. – РС Magazine March 25, – 1997. – 190 c. 23. Якобсон А. Мечты о будущем программирования. Открытые системы. – М.: – 2005. – № 12. – С. 59–63. 24. Летичевский А.А, Маринченко В.Г. Объекты в системе алгебраического программирования // Кибернетика и системный анализ. – 1997 .– № 2. – С. 160–180. 25. Летичевский А.А., Капитонова Ю.В., Волков В.А., Вышемирский В.В., Летичевский А.А. (мл.). Инсерционное программирование // Там же. – 2003. – № 1.– С.12–32. 26. Инсерционное программирование / Летичевский А.А., Капитонова Ю.В., Волков В.А., Вышемирский В.В., Летичевский А.А. (мл.) // Кибернетика и системный анализ.– 2003, №1.– С.19-32. 27. Редько В.Н. Экспликативное программирование: ретроспективы и перспективы // Проблемы программирования. – 1998. – № 2. – С. 22–41. 28. Редько В.Н. Основания программологии // Там же. – 2000.– № 1. – С. 35–57. 29. Никитченко Н.С. Композиционно–номинативный подход к уточнению понятия программы // Там же. – 1999. – № 1. – С. 16–31. 30. Цейтлин Г.Е. Введение в алгоритмику. – Изд.–во Фара, 1999. – 310 с. 31. Глушков В.М., Цейтлин Г.Е., Ющенко Е.Л. Алгебра. Языки. Программирование. – Наук. Думка, 1974, 1989.–331с. 32. Ершов А.П. Введение в теоретическое программирование.–М.: Наука, 1959.–263с. 33. Дорошенко А.Ю., Фінін Г.С., Цейтлін Г.О. Алгеброалгоритмічні основи програмування.–К.:Наук.думка, 2004.–457с. 145 Розділ 6. МЕТОДИ ДОВЕДЕННЯ, ВЕРИФІКАЦІЇ І ТЕСТУВАННЯ ПРОГРАМ Сучасні напрями перевірки правильності програм – це формальні специфікації, методи доведення, верифікація і тестування. Наведемо їхній зміст. 1. Формальні специфікації з'явилися у програмуванні в 70-х роках минулого сторіччя. Вони подібні МП і надають засоби, що полегшують опис міркування про властивості і особливості програм у математичній нотації. Під специфікацією розуміють формальний опис функцій і даних програм, якими ці функції оперують. На формальних специфікаціях базуються методи доведення програм, які були започатковані працями з теорії алгоритмів А.А. Маркова [1], А.А. Ляпунова [2], схемами Ю.І.Янова [3] та формальними нотаціями опису взаємодіючих процесів К.А. Хоара [4] і ін. Для перевірки формальної специфікації програми застосовують математичний апарат для опису правильного розв’язку деякої задачі, для якої вона розроблена. Разом з специфікацією розробляються додаткові аксіоми [5–10], твердження про опис операторів і умов, так звані попередні умови або передумови, і постумови, що визначають заключні правили одержання правильного результату. 2. Доведення програм проводиться за допомогою тверджень, що складаються у формальній мові і слугують для перевірки правильності програми в заданих її точках. Набір тверджень, перед- і постумов використовується для перевірки отриманого результату у деякій точці програми. Якщо твердження відповідає скінченому оператору програми, то за допомогою постумови робиться остаточний висновок про часткову або повну правильність роботи програм. 3. Верифікація і валідація – це методи забезпечення перевірки й аналізу правильності виконання заданих функцій програми відповідно до заданих вимог замовника до них і системи у цілому. 4.Тестування – це метод виявлення помилок у ПС шляхом виконання вихідного коду на тестових даних, збирання робочих характеристик у динаміці виконання в конкретному операційному середовищі, виявлення різних помилок, дефектів, відмов і збоїв, викликаних нерегулярними, аномальними ситуаціями або аварійним припиненням роботи системи. Теоретичні засоби реалізуються як процеси програмування і перевірки правильності програмного продукту. На даний час процеси верифікації, валідації і тестування ПС регламентовані стандартом ISO/IEC–12207 [7] з життєвого циклу ПС. У деякій зарубіжній літературі процеси верифікації і тестування на практиці ототожнюються, вони орієнтовані на досягнення правильності програми. Наведені методи доведення, верифікації і тестування при перевірці правильності програм кваліфікуються такими загальними поняттями і діями. Доведення та верифікація коректності (правильності) виконуються за формальною специфікацією програми та за допомогою тверджень, передумов (обмежень вхідних параметрів програми) і постумов (обмежень вихідних параметрів програми), які утворюють незалежну від програми частину механізму її доведення. Ця частина специфікується, як правило, на тій же мові, що і програма. У ній застосовуються математичні операції (диз’юнкції, кон’юнкції, імплікації тощо), квантори існування і загальності та інші. Передумова – це обмеження на сукупність вхідних параметрів і постумови як обмеження на вихідні параметри. Передумова і постумова задаються предикатами, результатом яких є булева величина (true/false). Передумова істинна тоді, коли вхідні параметри входять в область припустимих значень даної функції. Постумова істинна тоді, коли сукупність значень задовольняє вимоги, щодо формального визначення критерію правильності одержання результату. Твердження формулюються на формальній математичній мові у вигляді додаткової доказової частини, що перевіряє правильність виконання програми в початковій, проміжній або кінцевій точках. Постумова – це обмеження з умов про кінцевий результат програми, відповідно до якого формулюється висновок про правильне завершення цієї програми. Під доведенням часткової правильності розуміють перевірку виконання програми за допомогою тверджень, які описують те, що повинна одержати ця програма, коли закінчиться її виконання відповідно до умов заключного твердження. Повністю правильною програмою щодо її опису і заданих тверджень буде така програма, яка частково правильна і її виконання завершується при всіх даних, що відповідають їй. Перевірка правильності методом тестування базується на функціональних тестах або наборах тестів, які створюються шляхом опису функцій і проектної інформації на процесах ЖЦ з урахуванням вимог, сформульованих на процесі аналізу предметної області. 5. Організаційна інфраструктура якісного проектування – це різні служби і діяльність груп фахівців, що планують процеси досягнення правильності програм (доказ, верифікація, тестування) з використанням описів тверджень, різних умов, а також тестових даних для спостереження за процесом доведення правильності програм, зокрема тестування, і збирання даних про відмови і помилки програм для їхнього використання при оцінюванні показників якості. Далі зазначені напрями досягнення правильності програм розглядаються більш детально. 6.1. Мови специфікації програм і їхня класифікація Мови формальної специфікації, які використовуються для формального опису властивостей виконання програм шляхом завдання тверджень та перед і постумов, є мовами вищого рівня щодо мов алгоритмічного програмування, які можуть використовуватися для опису програми, для якої створюється доказ. У загальному випадку формальна специфікація програми – це однозначний специфікований опис програми за допомогою математичних понять, термінів, правил синтаксису і семантики формальної мови. Опис деякої задачі являє собою сукупність її формальної специфікації та необхідних для доведення аксіом, тверджень, перед- і постумов та інших формалізмів. Всі ці описи при реалізації вимагають не систему програмування з МП, а спеціальний програмно реалізований математично орієнтований апарат доведення програм, зокрема інтерпретатори або метасистеми. Існують різні підходи до класифікації мов специфікації, що наведені на рис.6.1. Розділ 6 147 Рис.6.1. Категорії формальних мов специфікації Нижче розглянуто основні мови специфікації, класифіковані за сферою застосування. Універсальні мови специфікації – VDM, Z, RAISE, Spec# мають загально математичну основу з такими засобами: 1) логіки першого порядку, включаючи квантори; 2) арифметичні операції; 3) множини і операції над множинами; 4) описи послідовностей (кортежів, списків) і операції над ними; 5) описи функцій і операцій над ними; 6) описи деревоподібних структур; 7) засоби побудови моделей областей; 8) процедурні засоби мов програмування (оператори присвоювання, циклу, вибору, виходу); 9) операції композиції, аргументами і результатами яких можуть бути функції, вирази, оператори; 10) механізм конструювання нових структур даних. Мови специфікації предметних областей (доменів) у програмуванні: 1) специфікації доменів; 2) описи взаємодій і паралельного виконання; 3) специфікації мов програмування і трансляторів; 4) специфікації баз даних і знань; 5) специфікації пакетів прикладних програм тощо. Мови специфікації специфіки доменів DSL (Domain Specific Language) призначені для формалізованого опису задач в термінах предметної області, що підлягає моделюванню. Ці мови можна підрозділити на зовнішні і внутрішні. Зовнішні мови (типу UML, OWL і ін.) за рівнем вищі мов програмування і відповідають, наприклад, предметно-орієнтованої мові DSL, яка використовується для подання абстрактних понять і задач ПрО. Їхній опис трансформується до понять деякої внутрішній мові або мови програмування спеціальними генераторами або текстовими редакторами. Внутрішні мови – мови опису специфічних задач обмеженим синтаксисом і семантикою потребують препроцесорів для перебудови цього опису до базової мови програмування. Специфікації опису взаємодій і паралельного виконання окремих процесів систем ПрО також добре подаються мовами DSL, наприклад, подібно – діаграм UML. Мови програмування предметної області, доповнені засобами і механізмами технологій. Метапрограмування є ефективним засобом автоматизації специфікацій розроблених програм і в даний час знаходять широке застосування у галузі інформаційних технологій. Формальні мови специфікації мов програмування спочатку застосовувалися при розробленні трансляторів. Так зазвичай синтаксис мови програмування описувався КС-граматиками у формі Бекуса–Наура. Такого типу мови є метамовами. Для специфікації семантики мов програмування використовуються формалізми рівностей. Техніка опису мов програмування базується на атрибутних граматиках і абстрактних типах даних з використанням денотаційних, алгебраїчних і атрибутних підходів. Як мови специфікації трансляторів, а також систем реального часу, де правильність і точність виконання програм є головними, використовують мови Z, VDM, RAISE. Мови специфікації з орієнтацією на засоби програмування базуються на рівностях і підстановках з операційною семантикою (Лісп, Рефал); логічні мови; мови операцій (АPL) над послідовностями і матрицями; табличні мови; мережі, графи та ін. Мова логіки предикатів використовується для запису передумов і постумов, інваріантів і процесу верифікації (наприклад, Пролог). Для визначення семантики рівності застосовують денотаційний, операційний і аксіоматичний опис. Операційна семантика пов'язана з підстановками (заміна, продукція) і визначається в термінах операцій, що призводять до обчислень алгоритмів. При цьому фіксується порядок і динаміка виконання операцій програми. У денотаційному підході до семантики надається перевага статичному опису об'єктів у термінах математичних властивостей, а у аксіоматичному – специфікації властивості об'єктів у рамках деякої логічної системи, що містить у собі правила виведення формул та/або інтерпретацій. Окрім наведеної класифікації мов специфікацій, існують інші. Наприклад, можлива класифікація специфікацій за способом виконання: – виконувана (executable), – алгебраїчна (algebraic), – сценарна (use case or scenarios), – в обмеженнях (constraints). Виконувані специфікації припускають розроблення прототипів систем для досягнення встановленої мети (VDM, SDL, RSL). Алгебраїчні специфікації та мови SDL, RSL містять у собі механізми опису аксіом і тверджень, які призначені для доведення специфікованих програм. Сценарні специфікації (UML) дозволяють описувати різні способи можливого застосування системи. Програмування в обмеженнях використовують перед- і постумови для опису даних, операцій, інваріантів даних програм, що доводяться. 6.1.1. Мова формальної специфікацій – VDM Мова специфікації VDM (Vienna Development Method) була розроблена у віденській лабораторії компанії IBM і призначалася для опису мов типу ПЛ/1, Розділ 6 149 трансляторів і систем із складними структурами даних. У мові специфікується правильна програма і набір тверджень для її доведення [7, 8]. Мова містить у собі такі типи даних: Х – натуральні числа з нулем; N – натуральні числа без нуля; Int – цілі числа; Bool – булеві; Qout – рядки символів; Token – знаки і спеціальні позначення операцій. Функція специфікує властивості структур даних і операцій над ними – апплікативно (функціонально) або імперативно (алгоритмічно). Наприклад, функції min у мові VDM описують двома способами: min N1 N2 N3, min (N1 N2) = if N1 N2 then N3. Об'єкти мови VDM: множини, дерева, послідовності, відображення, сконструйовані складні структури. Множина: X–set і операції , , , і ін. Правило: х А буде коректним тільки тоді, коли А є підмножиною множини, якій належить х. Дистрибутивне об'єднання підмножин покажемо на прикладі: union {(1, 2), (0, 2), (3, 1) } = (0, 1, 2, 3). Списки (послідовності): Х – операція, len – довжина списку, inds – номери елемента в списку. Наприклад, inds lst =(i X [f i len]). Узяття першого (голови) елемента списку – hd і залишку (хвоста) після видалення першого елемента із списку – tl. Наприклад, hd (а, b, с, d) = (a), tl (а, b, с, d) = (b, с, d). Дерево: mk об'єднує послідовності, множини і відображення. Елементи дерев можуть конструюватися. Наприклад, час 10.30 – конструкція let mk, час (h, m) = t, tin визначає значення h = 10, а m = 30. Відображення: map – таблиця з ключів і значень. Операція dom будує множину ключів, rng – множину його значень. Специфікація програми у VDM – це опис інваріантних властивостей, наприклад, inv – функція, аргументи і опис її операцій. Перевірки специфікації – це і перед- і постумови, твердження, які специфікуються засобами VDM, і мають таку семантику тлумачення у ньому. Передумова – це предикат з операцією, до якої звертається інваріант програми після отримання початкового стану для визначення правильності виконання або фіксації помилкової ситуації. Твердження – це опис операцій перевірки правильності інваріанта програми в різних її точках. Постумова – це предикат, який є істинним після виконання передумови, завершення поточних операції в заданих точках при виконанні інваріантних властивостей програми. Нижче наведено покрокову деталізацію специфікації програм мовою VDM: 1. Визначення термінів, якими буде специфікуватися програма. 2. Опис понять і об'єктів, для позначення яких використовується денотат, що ідентифікується за допомогою деякого імені (або фрази). 3. Опис інваріантних властивостей програми. 4. Визначення операцій над структурами програми (наприклад, ввести об'єкт, видалити і ін.), що змінюють її стан і збереження інваріантних властивостей. 5. Розроблення формальних умов виконання інваріанта програми та специфікація передумов, постумов, а також тверджень щодо виконання інваріанта програми. 6. Статичний огляд інваріанту програми щодо специфікованого формалізму доведення цього інваріанта. 7. Використання діючих CASE-засобів, що забезпечують виконання процесу верифікації програм. |