Логіка Гоара: відмінності між версіями
| [перевірена версія] | [перевірена версія] |
Вилучено вміст Додано вміст
Олюсь (обговорення | внесок) мНемає опису редагування |
MobyVan (обговорення | внесок) м replaced: в якості → як (2) за допомогою AWB |
||
Рядок 13:
В 1976 році вийшла книга Е. Дейкстри «'''''Дисципліна програмування»''''', в якій пропонується метод доведення правильності програми.
Суть методу полягає в тому, щоб будувати програму разом з доведенням, причому доведення повинно випереджати побудову програми.
Е.Дейкстр визначив для простої мови програмування слабкі передбачення і показав, як їх можна використовувати
== Основні ідеї Гоара ==
Рядок 23:
* Правило виводу каже, що можна підсилити перед і послабити постумову якщо нам це знадобитися. Немає сенсу волокти через всю програму якесь твердження, яке не допомагає вирішити поставлене завдання.
* Оператор розгалуження або просто if. Його умовно можна розбити на дві гілки then і else. Якщо до предумови додати істинність логічного умови (те, що стоїть під if), то після виконання гілки then повинна слідувати постумова. Аналогічно, якщо до передумовою додати заперечення логічного умови (те, що стоїть під if), то після виконання гілки else має слідувати постумова.
* Оператор циклу. Це саме нетривіальне і складне, оскільки цикл може виконується багато разів і навіть не скінчиться. Щоб вирішити проблему можливо багаторазового повтору тіла циклу вводять інваріант циклу. Інваріант циклу це те, що істинно перед його виконанням, істинно після кожного виконання тіла циклу і отже істинно і після його закінчення. Передумова для оператора циклу це просто його інваріант циклу. Якщо істинна умова продовження циклу (те, що стоїть під while), то після виконання тіла циклу повинна слідувати істинність інваріант циклу. В результаті після закінчення циклу маємо
* Оператора циклу з повною коректністю. Для цього до попереднього пункту додають обмежувальну функцію, за допомогою якої легко довести, що цикл буде виконуватися обмежену кількість разів. На неї накладають умови, що вона завжди >=\nbsp;0, суворо убуває після кожного виконання тіла циклу і в точності =\nbsp;0, коли цикл закінчується.
* Програму, що працює правильно можна написати дуже багатьма способами, а також вона у великій кількості випадків буде ефективною. Це свавілля і саме воно він ускладнює програмування. Для цього вводять стиль. Але цього виявляється мало. Для багатьох програм (наприклад, пов'язаних побічно з життям людини) потрібно довести і їх коректність. Виявилося, що доказ коректності робить програму дорожче на порядок (приблизно в 10 разів).
| |||