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