Студопедия
Контакти
 


Тлумачний словник

Реклама: Настойка восковой моли




Авто | Автоматизація | Архітектура | Астрономія | Аудит | Біологія | Будівництво | Бухгалтерія | Винахідництво | Виробництво | Військова справа | Генетика | Географія | Геологія | Господарство | Держава | Дім | Екологія | Економетрика | Економіка | Електроніка | Журналістика та ЗМІ | Зв'язок | Іноземні мови | Інформатика | Історія | Комп'ютери | Креслення | Кулінарія | Культура | Лексикологія | Література | Логіка | Маркетинг | Математика | Машинобудування | Медицина | Менеджмент | Метали і Зварювання | Механіка | Мистецтво | Музика | Населення | Освіта | Охорона безпеки життя | Охорона Праці | Педагогіка | Політика | Право | Програмування | Промисловість | Психологія | Радіо | Регилия | Соціологія | Спорт | Стандартизація | Технології | Торгівля | Туризм | Фізика | Фізіологія | Філософія | Фінанси | Хімія | Юриспунденкция

Методи доведення правильності програм

Загрузка...

Формальні методи тісно пов'язані з математичною специфікацією, верифікацією і доведення правильності програм. Ці методи містять математичну символіку, формальну нотацію і апарат виведення. Правила доведення є громіздкими і тому на практиці рідко використовуються рядовими програмістами. Проте з теоретичної точки зору вони слугують розвитку логіки застосування математичного методу індукції в процесі перевірці правильності програм.

Базові методи доказу. Відомо багато методів доказу специфікацій програм, деяким з них дамо короткий зміст.

Метод Флойда заснований на визначенні умов для вхідних і вихідних даних і полягає у виборі контрольних точок у програмі, яка доводиться, таким чином, щоб шлях проходження перетинав хоч б одну контрольну точку. Для цих точок формулюються твердження про стан і значення змінних у них (для циклів ці твердження повинні бути істинними при кожному проходженні циклу – інваріанта).

Кожна точка розглядається для індуктивного затвердження того, що формула залишається істинною при поверненні програми в цю точку, і залежить не тільки від вхідних і вихідних даних, але і від значень проміжних змінних. На основі індуктивних тверджень і умов на аргументи програми створюються твердження з умовами перевірки правильності цієї програми в окремих її точках. Для кожного шляху програми між двома точками встановлюється перевірка на відповідність умов правильності і визначається істинність цих умов при успішному завершенні програми на даних, що задовольняють вхідним умовам.

Метод Хоара – це вдосконалений метод Флойда, заснований на аксіоматичному описі семантики мови програмування початкових програм. Кожна аксіома описує зміну значень змінних за допомогою операторів цієї мови. Формалізація операторів переходу і викликів процедур забезпечується за допомогою правил виводу, що містять індуктивні вислови для кожної точки і функції початкової програми.

Метод Маккарті полягає у структурній перевірці функцій, що працюють над структурними типами даних, структур даних і шляхів переходу під час символьного виконання програм. Ця техніка включає моделювання виконання коду з використанням символів для змінних даних. Тестова програма має вхідний стан, дані і умови її виконання.



Интернет реклама УБС

Виконувана програма розглядається як серія змін станів. Саме останній стан програми вважається вихідним станом і, якщо він одержаний, програма вважається правильною. Даний метод забезпечує високу якість початкового коду.

Метод Дейкстри пропонує два підходи до доказу правильності програм. Перший підхід заснований на моделі обчислень, що оперує з історіями результатів обчислень програми, аналізом шляхів проходження і правил оброблення великого об'єму інформації. Другий підхід базується на формальному дослідженні тексту програми за допомогою предикатів першого порядку. У процесі виконання програма одержує деякий стан, який запам'ятовується для подальших порівнянь.

Основу методу складає математична індукція, абстрактний опис програми і її обчислення. За допомогою цього методу можна довести істинність деякого припущення Р(n) залежно від параметра n для всіх n ³ n0, і тим самим довести випадок Р (n0). Виходячи з істинності Р(n) для будь-якого значення n, доводиться Р(n+1), що достатньо для доказу істинності Р(n) для всіх n ³ n0.

 


Читайте також:

  1. Cisco Packet Tracer - Знайомство з програмою. Інтерфейс
  2. I. Введення в розробку програмного забезпечення
  3. I. ЗАГАЛЬНІ МЕТОДИЧНІ ВКАЗІВКИ
  4. II. Вимоги до складання паспорта бюджетної програми
  5. II. Із програм для 11 класу
  6. II. ПРОГРАМА КУРСУ
  7. II.1 Програмне забезпечення
  8. III. Етапи розробки програмного забезпечення
  9. III. Навчально-програмний етап.
  10. III. Програма
  11. III. Програма
  12. WEB ПРОГРАММИРОВАНИЕ

Загрузка...



<== попередня сторінка | наступна сторінка ==>
Концепторна мова специфікації | Модель доказу програми за твердженнями

Не знайшли потрібну інформацію? Скористайтесь пошуком google:


 

© studopedia.com.ua При використанні або копіюванні матеріалів пряме посилання на сайт обов'язкове.


Генерація сторінки за: 0.003 сек.