Без заголовка

Выход видится в том, что все такое документирование должно делаться специальными программами, которые должны пробовать восстановить по тексту программы такое документирование, а затем использовать его для доказательства правильности программы -- и для софта в последние годы в таком инструментарии прошел значительный прогресс. "The C language is particularly rich with ways of writing a program that totally hide the original design intent." - Stanley Chow Для императивных языков это нереально.