История изменений
Исправление AndreyKl, (текущая версия) :
То есть для каких-либо дополнительных утверждений о зависимостях параметров и результатов внутрь транслированного тела функции лезть не надо.
Верно.
В минусе только то, что функция становится минимальной единицей: хочешь что-то утверждать про кусок кода в функции, выноси в отдельную.
В принципе можно вынести из тела функции кусок и сформулировать о нём утвреждение, почему нет. Потом это можно использовать для доказательства какого то утверждения о функции (частью тела которой является вынесенный код). Но это детали процесса, там как удобнее.
Исходная версия AndreyKl, :
То есть для каких-либо дополнительных утверждений о зависимостях параметров и результатов внутрь транслированного тела функции лезть не надо.
Верно.
В минусе только то, что функция становится минимальной единицей: хочешь что-то утверждать про кусок кода в функции, выноси в отдельную.
В принципе можно вынести из тела функции кусок и сформулировать о нём утвреждение, почему нет. Потом это можно использовать для доказательства какого то утверждения о функции (частью тела которой является вынесенный код). Но это детали процесса, там как удобнее.