Обсуждение

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

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

А чо ты его латиницей пишешь? Человек в русскоязычных программыстских кругах давно известный, Хоар его фамилие. Венгр, кажется, по происхождению.

У юраузеров вечные проблемы с кэшированиям iframe'ов. Которые использутся для медиа в жж. Можно поинтересоваться, у вас какой браузер/версия?

У меня Firefox свежайшей (3.0.11) версии.

А я часто имена латинницей пишу -- не только его. Насчет венгра, правда, сильно сомневаюсь. Born in Colombo (Ceylon, now Sri Lanka) to British parents (http://en.wikipedia.org/wiki/C._A._R._Hoare).

Как я понимаю, алгоритмически разрешать просто придется в каждом проходе, включая внутри циклов...

Как я понимаю, ровно в этом месте и наступает стремительный прогресс :) Или они в Майкрософт начали писать Виндоуз на функциональных или логических языках? 8-()

Нет, просто они используют грубую силу. Прогресс конечно тоже есть. Но сами микрософтовцы (микрософт ресерчевцы) говорят: фрейм кондишенз - это самая жопа. Фрейм кондишенз - это ограничения на состояния массивов/кучи, ну т.е. как раз императивка. Прогресс безусловно тоже есть, тут они молодцы. В частности у них есть детектор инвариантов. Это все помогает, но стратегически они завязнут во фрейм кодишенз. Т.е. рано или поздно им придется уходить от императивки в сторону функционалки. Но я очень сомневаюсь, что они смогут это сделать - все таки корпоративная культура очень сильно давит. Грубо говоря это должна быть другая компания, типа Гугля, а с Микрософта уже побежал топ-менеджмент, включая Билла. С Вистой они облажались совмесем. Так что я думаю, что Микрософт уже не умирающая компания. А вот Микрософт Рисеч думаю выживет в том или ином виде, это что-то другое, не Микрософт.

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

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

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

Ну я согласен в том, что доказательство программ синергирует с генерацией программ. Это действительно так и есть даже фундаментальный результат, что по конструктивному доказательству спецификации можно сгенерировать программу, ее реализующую. Но вот с классическим программированием идет война - как сам Хоар говорит, тестирование конфликтует с верификацией.

А, ну, м.б., я его с Хааром перепутал (который в теории меры). Но человек известный во времена моей ВМК-шной юности.