Небольшой пост в блоге Бертранда Мейера под названием “Specification Explosion” (выделение жирным мое):
At a Microsoft Software Verification summer school [1] in Moscow on July 18 — the reason why there was no article on this blog last week — Stefan Tobies, one of the lecturers, made the following observation about the specification effort needed to produce fully verified software. In his experience, he said, the ratio of specification lines to program lines is three to one.
Т.е. на прошедшем 18 июля 2011 в Москве мероприятии под названием Microsoft Software Verification summer school один из лекторов, Стефан Тобиес, поделился своими наблюдениями о соотношении количества строк спецификаций к количеству строк в программе – у него получается 3:1.
Т.е. для того, чтобы получить верифицируемую программу требуется, чтобы спецификация для нее была в три раза больше объема самой программы.
Думаю, что при таких раскладах в ближайшие десятилетия годы вопрос о верификации подавляющего большинства коммерчески разрабатываемого ПО даже не будет выноситься на повестку дня.
Они там разделяли ПО как минимум на 3 уровня: критическое, бизнес, обычное.
ОтветитьУдалитьДля бизнес и обычного ПО, да, пока рановато.
Но можно же ПО специфицировать не полностью, да и вообще вопрос о полноте спецификации (и соответствия программы) довольно философский. Это все равно сильно поможет для тестирования/верификации.
@67108864:
ОтветитьУдалитьФилософский, конечно. Но объемы ПО постоянно растут и, мне кажется, вопрос о том "а правильно ли вообще ПО работает" становится все сложнее и сложнее. Верификация уже давным-давно рассматривается как один из способов дать ответ на этот вопрос. И как раз интересно было узнать о приблизительной трудоемкости получения этого ответа на данном этапе.
по-моему выход в том, чтобы аналогично type inference научиться выводить доказательства
ОтветитьУдалить@имя:
ОтветитьУдалитьПроблема с верификацией, как мне кажется, лежит совсем не в области технических (технологических) инструментов.
В обычных программах достаточно часто проявляются ситуации, когда программа вдруг делает неожиданные вещи. Ты думаешь, что это ошибка в коде, но на самом делел код делает именно то, что и написал. Просто ты не думал именно о таком стечении обстоятельств.
Так вот для верификации программ об этом нужно не только подумать, но и определить реакцию кода. А затем зафиксировать как внешние условия, так и результат реакции в том или ином формальном виде (будь то спецификация на каком-то языке или система типов для конкретной программы).
И, как показывает практика, на вот этот вот тчательное обдумывание и проработку/формализацию всех деталей времени/усилий требуется очень много. Что, мне кажется, объективно и никуда от этого не уйти.