Логіка Гоара: відмінності між версіями
| [неперевірена версія] | [неперевірена версія] |
Вилучено вміст Додано вміст
Рядок 18:
Основою для логіки виведення правильних програм служать аксіоми [[Тоні Гоар|Гоара]]. Вони допускають інтерпретації в термінах програмних конструкцій.
Сформулюємо аксіоми [[Тоні Гоар|Гоара]], які визначають передумови як достатні умови, які гарантують, що виконання відповідних операторів при вдалому завершенні приведе до бажаних після умов.
=== Аксіома про порожній оператор ===
Аксіома про порожній оператор каже нам що він не змінює стан програми, тому що було правдою до його виконання, залишається таким же і після.
: <math> \frac{}{\{P\}\ \textbf{skip}\ \{P\}} \!</math>
=== Аксіома про присвоєння ===
Аксіома про присвоєння каже що після присвоєння для змінної виконується предикат, який виконувався для правої частини оператора присвоєння:
: <math> \frac{}{\{P[E/x]\}\ x:=E \ \{P\} } \!</math>
Тут <math>P[E/x]</math> позначає вираз ''P'' у якому всі [[вільна змінна|вільні входження]] змінної ''x'' були замінені виразом ''E''.
Рядок 34 ⟶ 35:
Приклади правильних трійок:
:* <math>\{x+1 = 43\}\ y:=x + 1\ \{ y = 43 \}\!</math>
:* <math>\{x + 1 \leq N \}\ x := x + 1\ \{x \leq N\}\ \!</math>
=== Правило композиції ===
Правило композиції застосовується до послідовно виконуваних програм ''S'' та ''T'', де ''S'' виконується до ''T'' і записується ''S;T''.
: <math> \frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \!</math>
Наприклад, розглянемо такі два присвоєння:
: <math>\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}</math>
та
: <math>\{ y = 43\} \ z:=y\ \{z =43 \}</math>
З правила композиції:
: <math>\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}</math>
=== Правило умови ===
З трійки для умовного оператора можна вивести дві трійки: одну для випадку істинності умови, іншу для її хибності:
: <math>\frac { \{B \wedge P\}\ S\ \{Q\}\ ,\ \{\neg B \wedge P \}\ T\ \{Q\} }
{ \{P\}\ \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif}\ \{Q\} } \!</math>
=== Правило висновків ===
Передумову та/або постумову можна замінити, якщо для них виконуються певні [[імплікація|імплікації]]:
: <math>
\frac { P^\prime \rightarrow\ P\ ,\ \lbrace P \rbrace\ S\ \lbrace Q \rbrace\ ,\ Q \rightarrow\ Q^\prime }
{ \lbrace P^\prime\ \rbrace\ S\ \lbrace Q^\prime\rbrace }
Рядок 68 ⟶ 69:
=== Правило While ===
: <math>\frac { \{P \wedge B \}\ S\ \{P\} }
{ \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} }
\!</math>
Рядок 76 ⟶ 77:
=== Правило While для тотальної коректності ===
:: <math>
\frac { <\;\textrm{is\ well-founded,}\;[P \wedge B \wedge t = z ]\ S\ [P \wedge t < z ]}
{ [P]\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ [\neg B \wedge P] }
\!</math>
:: В цьому правилі на додачу до інваріанта циклу, також доводять завершуваність додаванням [[варіант циклу|варіанта циклу]] (тут ''t''), чиє значення строго спадає згідно з [[:en:well-founded relation]] протягом кожної ітерації. Через те що відношення "&
Аксіоми можна використовувати для перевірки узгодженості передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов'язано з семантикою програми
::
== Приклади ==
| |||