Здравствуйте, 0x7be, Вы писали:

0>То есть нет возможности вызвать функцию обработки данных до её загрузки или если загрузка обломалась.
0>И нет возможности вызвать функцию скачки результата, если данные не были обработаны.

А теперь представь себе, что если загрузка обломалась, то надо выполнить операцию восстановления работоспособности сервера (или БД), после чего окажется, что загрузка уже прошла (для БД это странно, конечно, но в других случаях возможно, что некая инициализация обязана не только открыть канал, но и загрузить первую порцию данных).

Или если данные не обработаны, то нельзя скачивать результат, но можно (и нужно!) произвести ренинициализацию БД. Данные неправильно считаны, надо все с начала делать. Опять же с БД маловероятно, а в другом случае может быть.

Понимаешь, в чем проблема. Логика действий , вообще говоря, зависит от того, как выполнены предыдущие действия. Она может быть сколь угодно сложной, и все ее варианты могут быть оценены только путем выполнения и изучения результатов. А ты хочешь каким-то образом без того, чтобы эти результаты получить, сделать вывод о том, правильная ли эта логика (== потребовать от компилятора. чтобы он ее верифицировал).

Разумеется, есть множество алгоритмов или задач, которые допускают такую верификацию. Если логика достаточно проста, иными словами, этих путей исполнения немного (а лучше всего 1), то можно до исполнения определить, верна ли логика. Но в общем случае нет.

Вот тебе простой пример (из какой-то книги, которую я в молодости читал). Алгоритм одевания мужчины. Весь перечислять не буду, но ясно, что носки нужно надеть раньше, чем ботинки, а пиджак позже, чем рубашку. Хотя и тут вариантов много. Можно в таком порядке : носки, рубашку, пиджак , брюки,, ботинки. А можно и в таком порядке — носки, брюки, рубашку, пиджак, ботинки . А впрочем, и так можно, хотя и странно : рубашку, пиджак, брюки, носки, ботинки. Хотя после 3-го этапа выглядеть будешь весьма глупо

Вот и посчитай, сколько тут вариантов, и попробуй оцени без выполнения, правилен ли выбранный. Теоретически возможно. Построить граф всех правильных путей и проверить, есть ли наш путь в этом графе. Но возни тут намного больше, чем если проверить наш алгоритм на коллеге

А ведь пример простенький, и предметов одежды меньше десяти, и условий нет. А когда еще условия появляются ? Не удалось повязать галстук — вместо шляпы изволь одеть кепку. Не надел носки — в ботинках идти нельзя, а можно только в шлепанцах, а это значит, что нельзя и пиджак с галстуком надевать. И т.д. И т.п.

ИМХО все это чистый академизм, не имеющий отношения к реальной работе. Теоретизировать можно, а потом все это уйдет в архив вполне благополучно. Как с Сигуларити. Мне ее WolfHound пару лет назад усиленно пропагандировал, мол, новое слово, ОС на основе управляемого и верифицируемого кода. Новое — да, но и только. А теперь говорят, что ее вовсе закрыли (http://rsdn.ru/forum/life/4229495.1.aspx

Автор: Романов Михаил
Дата: 11.04.11

). Впрочем, если и не закрыли, то все равно толку мало...