slava писал(а):
Как то читал статью о "структурных переходах" (не помню ни автора ни точного названия).
В которой утверждалось, что переходы вперед и во внешний контекст являются "структурными".
Т.е., break, continue, throw-catch и даже обычный goto удовлетворяющий этим условиям можно считать структурными переходами.
К сожалению не помню пытались ли авторы доказать применимость формальных методов для доказательства корректности алгоритмов с такими "структурными переходами".
Насчёт структурности с авторами можно поспорить, а вот насчёт выбранного ими метода можно сказать следующее. Это топологическая сортировка. Её использование позволяет быть уверенным, что не придётся иметь дела с зацикленностями в программе из-за подобных переходов (goto). В математике, думаю, можно найти и доказательства этого факта.