і процес генерації тестів на їх Основі.
Під формальність спеціфікацією розуміють математичний описание програмної або апаратної системи, котра может буті реалізована на Основі цього опису. Спеціфікується что винна делать система, а не як вона винна це делать.
Додатковий бонусом від формалізації вимог є по-перше, ті, что ПРОТЯГ процеса їх Перетворення віявляються Недоліки - неточності або протіріччя у їх тексті, тоб проводитися їх статичність тестування . По-друге, вимоги у такому вігляді мают Більшу трівалість життя, чем у вігляді знань окрем індівідів, а такоже потребуються Менш зусіль для ПІДТРИМКИ, чем вимоги сформульовані на природній мові - что виробляти до СКОРОЧЕННЯ витрат коштів на підтрімку.
Серед існуючіх формальних моделей вимог, поведінкі та оточення програмного забезпечення для АНАЛІЗУ его властівостей віділяють наступні групи логіко-алгебраїчні , операційні та проміжні.
Логіко-алгебраїчні МОДЕЛІ . При моделюванні ПЗ модель такого типу опісує Деяк набор его властівостей, Які могут змінюватіся з годиною, альо НЕ Дає точного уявлення про ті, за рахунок чого змінюються ЦІ Властивості. Відмінність между логічнім та алгебраїчнім чисельно й достатньо Умовне, альо, Дещо спрощуючі, можна вважаті, что логіка має Справу з тверджень в рамках якоїсь мови, а алгебра - з рівностямі та нерівностямі, Які побудовані в деякій мові віразів. У первом випадка переважно про «єктом уваги є Твердження, хібні або істінні, а в іншому - вирази або терми, пов» язані з якімось типом.
Приклади логічніх чисельно Такі:
Обчислення висловлювань . У ньом є атомарні висловлювань, Які Можливо залежався від об «єктніх змінніх, а такоже логічні зв» язки («і», сполучення), («або», діз'юнкція), («не», заперечення), => («Отже», імплікація),=(еквівалентність), с помощью якіх можна з одних висловлювань будуваті Інші, більш складні.
Обчислення предікатів додає ПЕРЕЛІК висловлювань можлівість використовуват КВАНТОР по об «єктнім зміннім для побудова новіх тверджень. Квантори в цьом обчісленні бувають двох Видів - «загальності» та «Існування». У чісленні предікатів крім об »єктніх змінніх є функціональні и предікатні. Перші являютя собою різноманітні Функції, результат! Застосування Функції до об «єкта - об» єкт. Другі невізначені Твердження, результатом їх! Застосування до об «єкту має буті або« true », або« false ». У котрі тіпізованому обчісленні ВСІ об »єкти рівноправні, Функції та предикати могут прійматі будь-які про« єкти в якості аргументів. У тіпізованіх чисельно КОЖЕН об »єкт має тип, а функціональні и предікатні змінні - сигнатуру, тоб список тіпів параметрів и тип результату для функцій. Відповідно, будуваті формули можна позбав дотрімуючісь відповідності тіпів параметрів типам віразів, Які підставляють на місце ціх параметрів.
Обчислення предікатів більш високих порядків. У ціх обчисления можна використовуват КВАНТОР НЕ Тільки по об «єктнім зміннім, альо и по функціональнім або предикативного. Наприклад, визначення рівності об »єктів іноді формулюється так:, два об'єкти Рівні, ЯКЩО будь-яке Твердження одночасно Виконано б або не Виконано для них обох.
? чи...
