Вікіпедія

Логіка Гоара: відмінності між версіями

Інтерактивний перегляд історії
[неперевірена версія][неперевірена версія]
← Попереднє редагуванняНаступне редагування →
Вилучено вміст Додано вміст
ВізуальнийВікірозмітка
оформлення, правопис
Рядок 24:
Основна ідея Гоара дати для кожної конструкції імперативного мови перед і пост-умови записане у вигляді логічної формули. Тому і виникає у назві трійка — передумова, конструкція мови, пост-умовою.
 
* Ясно, що для порожнього оператора перед і постумови збігаються.
* Для оператора присвоювання в постусловіемпостумова крімокрім предусловияпередумови має враховувати факт, що значення змінної стало іншим.▼
 
* Для складеного оператора (в Python це відступи, в C це {}) маємо ланцюжок перед і постусловіемпостумов. ВУ результаті для складеного оператора можна залишити першийпершу передумовапередумову і останнєостанню постусловіемпостумову.▼
▲Для оператора присвоювання в постусловіем крім предусловия має враховувати факт, що значення змінної стало іншим.
* Правило виводу каже, що можна підсилити перед і послабити постусловіемпостумову якщо нам це знадобитися. Немає сенсу волочитиволокти через всю програму якесь твердження, яке не допомагає вирішити поставлене завдання.▼
 
* Оператор розгалуження або просто if. Його умовно можна розбити на дві гілки then і else. Якщо до предусловіюпредумови добавітьдодати істинність логічного умови (те, що стоїть під if), то після виконання гілки then повинноповинна следоватьпостусловіеслідувати постумова. Аналогічно, якщо до передумовою додати заперечення логічного умови (те, що стоїть під if), то після виконання гілки else має слідувати постусловіемпостумова.▼
▲Для складеного оператора (в Python це відступи, в C це {}) маємо ланцюжок перед і постусловіем. В результаті для складеного оператора можна залишити перший передумова і останнє постусловіем.
 * Оператор циклу. Це саме нетривіальне і складне, оскільки цикл може виконується багато разів і навіть не скінчиться. Щоб вирішити проблему можливо багаторазового повтору тіла циклу вводять інваріант циклу. Інваріант циклу це те, що істинно перед його виконанням, істинно після кожного виконання тіла циклу і отже істинно і після його закінчення. Передумова для оператора циклу це просто його інваріант циклу. Якщо істинноістинна умова продовження циклу (те, що стоїть під while), то після виконання тіла циклу повинна слідувати істинність інваріант циклу. В результаті після закінчення циклу маємо в якості постусловіяпостумови істінностьістинність інваріантінваріанту циклу і заперечення умови продовження циклу.▼
 
 * Оператора циклу з повною коректністю. Для цього до попереднього пункту додають обмежуєобмежувальну функцію, за допомогою якої легко довести, що цикл буде виконуватися обмежену кількість разів. На неї накладають умови, що вона завжди > = \nbsp;0, суворо убуває після кожного виконання тіла циклу і в точності = \nbsp;0, коли цикл закінчується.▼
▲Правило виводу каже, що можна підсилити перед і послабити постусловіем якщо нам це знадобитися. Немає сенсу волочити через всю програму якесь твердження, яке не допомагає вирішити поставлене завдання.
 Правильно* працюючуПрограму, що працює програмуправильно можна написати дуже багатьма способами, а також вона у великій кількості випадків буде ефективною. Це свавілля і саме воно він ускладнює програмування. Для цього вводять стиль. Але цього виявляється мало. Для багатьох програм (наприклад, пов'язаних побічно з життям людини) потрібно довести і їх коректність. Виявилося, що доказ коректності робить програму дорожче на порядок (приблизно в 10 разів).▼
 
▲Оператор розгалуження або просто if. Його умовно можна розбити на дві гілки then і else. Якщо до предусловію добавіть істинність логічного умови (те, що стоїть під if), то після виконання гілки then повинно следоватьпостусловіе. Аналогічно, якщо до передумовою додати заперечення логічного умови (те, що стоїть під if), то після виконання гілки else має слідувати постусловіем
 
▲ Оператор циклу. Це саме нетривіальне і складне, оскільки цикл може виконується багато разів і навіть не скінчиться. Щоб вирішити проблему можливо багаторазового повтору тіла циклу вводять інваріант циклу. Інваріант циклу це те, що істинно перед його виконанням, істинно після кожного виконання тіла циклу і отже істинно і після його закінчення. Передумова для оператора циклу це просто його інваріант циклу. Якщо істинно умова продовження циклу (те, що стоїть під while), то після виконання тіла циклу повинна слідувати істинність інваріант циклу. В результаті після закінчення циклу маємо в якості постусловія істінность інваріант циклу і заперечення умови продовження циклу.
 
▲ Оператора циклу з повною коректністю. Для цього до попереднього пункту додають обмежує функцію, за допомогою якої легко довести, що цикл буде виконуватися обмежену кількість разів. На неї накладають умови, що вона завжди> = 0, суворо убуває після кожного виконання тіла циклу і в точності = 0, коли цикл закінчується.
 
▲ Правильно працюючу програму можна написати дуже багатьма способами, а також вона у великій кількості випадків буде ефективною. Це свавілля і саме він ускладнює програмування. Для цього вводять стиль. Але цього виявляється мало. Для багатьох програм (наприклад, пов'язаних побічно з життям людини) потрібно довести і їх коректність. Виявилося, що доказ коректності робить програму дорожче на порядок (приблизно в 10 разів).
 
== Трійки Гоара ==
Отримано з https://uk.wikipedia.org/wiki/Логіка_Гоара