м;
2) максимальне використання результатів компіляції програми і, в Зокрема, інформації, що включається в лістинг компілятора;
В
3) замість повного синтаксичного розбору тексту програми, що перевіряється побудова для неї списку ідентифікаторів і списку операторів з вказівкою всіх їх необхідних ознак.
При відсутності інструментальних засобів контролю правдоподібності ця фаза статичного контролю також може об'єднуватися з візуальним контролем.
Четвертої формою статичного контролю програм є їх верифікація, тобто аналітичний доказ їх коректності.
У інтуїтивному значенні під коректністю розуміють властивості програми, свідчать про відсутність в ній помилок, допущених розробником на різних етапах проектування (специфікації, проектування алгоритму і структур даних, кодування). Коректність самої програми по відношенню до цілям, поставленим перед її розробкою (тобто ця відносна властивість ). Відмінність поняття коректності і надійності програм в наступному:
надійність характеризує як програму, так і її "оточення" (якість апаратури, кваліфікацію користувача і т.п. ); p> кажучи про надійність програми, звичайно допускають певну, хоч і малу, частку помилок в ній і оцінюють імовірність їх появи.
Надійність можна представити сукупністю наступних характеристик:
1) цілісність програмного засобу (здатність його до захисту від відмов);
2) живучість (здібність до вхідного контролю даних і їх перевірки в ході роботи);
3) завершеність (бездефектність готового програмного засобу, характеристика якості його тестування);
4) працездатність (здатність програмного засобу до відновлення своїх можливостей поле збоїв).
Очевидно, що не всяка синтаксично правильна програма є коректною у зазначеному вище сенсі, т. е. коректність характеризує семантичні властивості програм.
5
З урахуванням специфіки появи помилок в програмах можна виділити дві сторони поняття коректності:
1) коректність як точна відповідність цілям розробки програми (які відображені в специфікації) при умові її завершення або часткова коректність;
2) завершення програми, тобто досягнення програмою в процесі її виконання своєї кінцевої точки. p> Залежно від виконання або невиконання кожного з двох названих властивостей програми розрізняють шість задач аналізу коректності:
1) доказ часткової коректності ; p> 2) доказ часткової некоректність ; p> 3) доказ завершення програми;
4) доказ незавершення програми ; p> 5) доказ тотальної (повної) коректності (тобто одночасне рішення першої і третьої задач);
6) доказ некоректність (рішення другої або четвертої задачі).
Методи доказу часткової коректності програм як правило спираються на аксіоматичний підхід до формалізації семантики мов програмування. В даний час відомі аксіоматичні семантики Паскаля, підмножини ПЛ/1 і деяких інших мов.
Аксіоматична семантика мови про...
