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

[перевірена версія][перевірена версія]
Вилучено вміст Додано вміст
BunykBot (обговорення | внесок)
м Вікіфікація
Рядок 107:
{ [P]\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ [\neg B \wedge P] }
\!</math>
:: В цьому правилі на додачу до інваріанта циклу, також доводять завершуваність додаванням [[варіант циклу|варіанта циклу]] (тут ''t''), чиє значення строго спадає згідно з {{iwнп|Фундоване відношення|фундованим відношенням||well-founded relation}} протягом кожної ітерації. Через те що відношення «<» well-founded, кожна ітерація циклу перелічується спадними членами скінченного [[ланцюг (теорія порядку)|ланцюга]]. Також зауважте, що тут для позначення тотальної коректності використовуюються квадратні дужки. (Це одне з можливих позначень тотальної коректності.)
Аксіоми можна використовувати для перевірки узгодженості передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов'язано з семантикою програми.
::
 
== Приклади ==