?

Log in

November 2016   01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
cartoon

Миф о документации, продолжение

Posted on 2011.06.18 at 23:06

Comments:


Gaperton
gaperton at 2011-06-19 11:25 (UTC) (Link)
> Нет, это невозможно. По крайней мере никому в этом мире ещё не удавалось.

Теоретически, это (в некоторой степени) возможно, в случае, если код целиком генерируется из формальной спецификации, непротиворечивость и полнота которой доказывается.

Скажем, в университете нам преподавали Btoolkit. http://en.wikipedia.org/wiki/B-Method

Стоит отдельно отметить, что никто в здравом уме не будет считать разработку и применение таких методов как B-Method заслугой и результатом QA. :) У меня лично как-то язык не поворачивается. :)

Однако, даже в этом случае не исключено расхождение между спецификацией, и реальной ситуацией - тем, что на самом деле требуется. Так что не худо бы все-таки испытать софтину, разработанную с применением B-method-а. А вот разработотка "программы и методики испытаний" к ней - это уже задача QA. Как и сама проверка.
Lost In Paradox
localstorm at 2011-06-19 11:35 (UTC) (Link)
>код целиком генерируется из формальной спецификации, непротиворечивость и полнота которой доказывается

Я надеюсь непротиворечивость и полнота тоже совершенно автоматически и точно устанавливается за разумное время :) А то можно ведь ошибиться при доказательстве (такое вот часто бывало при доказательстве теоремы Ферма. Считается, например, что сам Ферма провел какое-то рассуждение, которые он посчитал очевидным, но при этом оно было не вполне корректно)

Но даже в этом случае, как справедливо замечено, возможны ошибки на уровне как изначальных предпосылок и так и требований к результату, которые формально будут соблюдены, но хэппе никто все равно не станет.

На практике же я не могу представить себе полного разделения между тем, кто придумывает как вести тестирование и тем, кто тестирует. Это сродни архитектору, который "архитектурит", а вот работу делают все остальные, при этом на код архитектор не смотрит.
Gaperton
gaperton at 2011-06-19 11:42 (UTC) (Link)
> Я надеюсь непротиворечивость и полнота тоже совершенно автоматически и точно устанавливается за разумное время :)

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

Этот курс был у моих друзей с другого потока. Им надо было написать квиксорт. Постоянно рассказывали об ощущениях, и матерились страшенно. :)

> На практике же я не могу представить себе полного разделения между тем, кто придумывает как вести тестирование и тем, кто тестирует. Это сродни архитектору, который "архитектурит", а вот работу делают все остальные, при этом на код архитектор не смотрит.

Ага. И сродни главбуху, который разрабатывает план счетов с типовыми проводками для операций, минимизируя налоги, но при этом не отвечает за бухучет.
Lost In Paradox
localstorm at 2011-06-19 11:47 (UTC) (Link)
Да было у меня что-то похожее. Самое сложное, при кажущейся очевидности, это описать требования. Пусть даже не квиксорт, а просто какой-нибудь сорт.

Как описать с использованием далеко не самого мощного выразительного средства концепцию, что были какие-то элементы, а потом их перенумеровали, но при этом не появилось ни новых элементов, ни старых не исчезло и при этом они стали упорядочены -- это сложно. Очень сложно для такой простой задачи.
Lost In Paradox
localstorm at 2011-06-19 11:57 (UTC) (Link)

Ради смеха

Я понимаю, что все понимают, что все это слишком далеко от практики, но тем не менее. Эта мысль мне показалась забавной.

Мне вот интересно, как тюнить первоманс в приложениях, созданных с применением B-Method? Это ж надо нехилое воображение иметь, чтобы написать такую формально корректную спеку, и чтобы код сгенерировался оптимальный. Это, наверное, только изобретателю этого кодогенератора по зубам...
hedgeov
hedgeov at 2011-06-19 17:52 (UTC) (Link)
Касательно формальной спецификации: был у меня практический опыт работы с кодом, генерированным из UML, непротиворечивого и полного. В общем там было всё ооооочень плохо :) Практическая рекомендация опытных коллег была такая: эта хрень точно и без ошибок умеет вот эту функцию выполнять, проверяли. Если тебе надо еще и вот это вот использовать -- напиши своё, то что есть ну очень кривое и не чинится за разумное время.
Previous Entry  Next Entry