Логіка Гоара: відмінності між версіями
[перевірена версія] | [перевірена версія] |
Вилучено вміст Додано вміст
м Вікіфікація |
→Правило While для тотальної коректності: вікіфікація |
||
Рядок 107:
{ [P]\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ [\neg B \wedge P] }
\!</math>
:: В цьому правилі на додачу до інваріанта циклу, також доводять завершуваність додаванням [[варіант циклу|варіанта циклу]] (тут ''t''), чиє значення строго спадає згідно з {{
Аксіоми можна використовувати для перевірки узгодженості передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов'язано з семантикою програми.
::
== Приклади ==
|