Previous Entry Share Next Entry
photo24

Про ёжика в тумане, зазнайство, языки программирования и вериги (repost)

Оригинал взят у vit_r в Про ёжика в тумане, зазнайство, языки программирования и вериги
Вынесу из комментариев к закрытому посту. Уж больно хорошо получилось.

vit_r
... чтоб не появлялось багов, спроектированное должно прямо генериться в код. Плюс должны быть тесты и проверки моделей. Я знаю отдельные случаи, где так и делается. Но методики не прижились. Потому что людей, способных мыслить абстрактно, очень мало.
...
xtUML, но его применяют только в embedded. Там сложности с выходом на GUI. Да и компиляторы моделей стоят столько, что проще нанять десять индусов.

Впрочем, будет работать любая методика, которая использует сообщения, конечные автоматы и таблицы переходов. Этот трюк изобретают вновь и вновь, потому что книжки старые никто не читает.


akuklev
Мы такое с sorhed'ом лет 7 назад изобрели и были феерически горды собой... пока в процессе имплементации не обнаружили книжку 1956 года ("Automatal models of multiagent systems", емнип), где это уже описано. :-)

Про подход при этом не знала ни университетская профессура, с которой я бурно обсуждал доказательства корректности, ни "старшие товарищи" из индустрии.

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

Да, ключевые слова от akuklev для желающих:
  • von Neumann multiagent formalism
  • Robin Milner
  • C.A.R. Hoare
  • Sally Shlaer и Stephen Mellor [сейчас идёт под маркой Executable UML (xtUML и xUML) - vit_r]
  • A. J. H. Simons
  • W. M. L. Holcombe
  • Complete functional testing using object machines
  • A theory of regression testing for behaviourally compatible object types


  • 1
dmih June 14th, 2013
Каждый раз, когда я в любой дискуссии с т.н. программистами говорю фразу "проверяемый код", на меня смотрят как на дебила.
Поэтому у нас 90% рабочего времени и состоит везде из отладки и 90% кода в любых проектах нормально с первого раза не работает в принципе. :(

max630 June 14th, 2013
Я могу догадаться, почему они на вас так смотрят. Потому что, условно говоря, 30% требований на момент написания софта не существуют (и это ещё очень оптимистично), ещё 30% не проверяемы в принципе, а 30% вроде проверяемы, но баги в используемых библиотеках приводят к тому что всё равно всё надо тестировать.

dmih June 14th, 2013
Вот вы ровно ту же самую фигню и написали. Проверяемый код - сразу тесты да ТЗ; событийная архитектура - а, вы про Erlang и т.д.
вот хочется взять что-нибудь тяжелое в ответ, простите. ничего личного.

akuklev June 14th, 2013
Мне доводилось в жизни писать "проверяемый код". Непроверяемым было только удобство и приятный внешний вид пользовательского интерфейса, но этим занимался отдел QA с систематизированным набором тестов и критериев. Этому не мешало то, что 40% требований на момент написания не существовало, не мешали и баги в сторонних библиотеках. Мешало строго говоря только одно: затратность разработки. Делать не частично, а полностью проверяемый код звездец как дорого. :(

dmih June 14th, 2013
Да его и не надо в проекте писать от начала и до конца; ну если конечно задачи такой не стоит.

Но надо же иметь в виду всё время, что проект должен поддерживать декомпозицию на какие-то понятные, компактные и проверяемые куски. И желательно иметь при этом в виду НЕ "функции покороче, покрытые тестами", а настроение в голове в целом. В этом отношении типичную ООП-шную перевитую лапшу, или скрипт-стайл программирование сверху вниз, например, к проверяемому виду свести сложнее, чем скажем event-driven, которая в декомпозированном виде фактически всю дорогу до конца и находится, даже в огромных проектах. Ну это просто короткий и условный пример.
Есть проекты, которые существенно склонны разъезжаться от изменений, а есть которые к ним устойчивы. Это не вопрос качества кода или количества комментариев или предсказуемости внешних библиотек; это просто у программиста в голове должна быть концепция о том, что по коду такого типа, для примера, можно провести доказательство корректности, более того это просто, а по коду этакого типа - нет, хоть ты что с ним делай (ну, не беря сложность вида квадратов и кубов от кол-во строк кода).

К внешним библиотекам это действительно имеет мало отношения, классическое отношение к багам никто не отменял. Более того, это к юнит-тестам тоже не имеет никакого отношения, юнит-тесты это другого типа костыль.

Вон по списку и вперед же. Они вам про автодоказательство теорем и прочее, и именно ЭТОМУ стоило бы посвятить заметную часть обучения программированию, а вы всё как на подбор опять, опять, опять, опять про юнит-тесты, QA и ТЗ, да тьфу.

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

max630 June 14th, 2013
А ответ простой - потому что можно и так. И это, как многим кажется, намного дешевле (и самое обидное - что часто действительно много дешевле, особенно).

(там ещё про электронику писали, так вот я слышал что производители той электроники пишут много запросов на софтовые воркераунды своих глюков, когда речь идёт о каком-то совместном девайсе)

mikkim08 June 14th, 2013
"Automatal models of multiagent systems

А это про что ? Просто интересно.

sab123 June 14th, 2013
Фигня на самом деле. Всякие такие Доказательства Правильности известны уже 50 лет как, а толку от них все еще ноль.

Max Desyatov June 14th, 2013
Пост о том, что толку ноль потому что никто их не читает. Если бы читали и применяли, вы бы не говорили "фигня на самом деле".

sab123 June 14th, 2013
Проблема в том, что их применять к чему-нибудь реального размера просто нет возможности. И за 50 лет эту возможность так никто и не придумал. Это даже если отвлечься от вопроса о том, что в массе своей такие "доказательства" - просто тавтологии. Оно доказывает, что формулировка А соответствует формулировке Б, но совершенно ниоткуда не следует, что формулировка Б дает правильное решение.

Это та же проблема, что и с тестированием с помощью моков: одна и та же хрень пишется два раза (во второй раз - с подглядыванием на первый), и предполагается, что типа протестировали.

akuklev June 14th, 2013
Нет, тавтологии это только искуственные примеры уровня достижений Хоара. В современном функциональном программировании речь идёт о корректности по построению, а не доказательствам корректности алгоритма отдельно от алгоритма. И корректные-по-построению функции даже существенной сложности на Agda и Idris писать уже можно. Но это только об алгоритмах, а не о системах.

Для систем подход совсем другой. Доказывать теоремы там вообще не о чем, потому что сформировать утверждение, которое мы пытаемся доказать, обычно _сложнее_, чем запрограммировать систему. Там речь идёт о том, чтобы строить систему таким образом, чтобы
а) её поведение можно было понимать в целом: это достигается
- высокой структурированностью поведения через диаграммы переходов, причём если система не может быть обозрена одним взглядом, её нужно разбить на подсистемы (а возможно и их ещё мельче), чтобы были диаграммы переходов разных масштабов,
- независимостью поведения на масштабе X от мелочей в коде в масштабе Y << X, и в особенности независимости large-scale поведения от мелких изменений в коде
б) в идеале, даже для очень сложных систем можно сделать полноценное покрытие всей диаграмы переходов юзкейсами.

Complete behavioural testing это и есть "доказательство корректности", в котором утверждение теоремы такое:
1) Заданный набор юзкейсов с точностью до вариации количественных параметров (там поведение системы продолжается по непрерывности) на 100% характеризует поведение системы в целом,
2) Во всех юзкейсах система ведет себя именно так, как желают того заказчики (составители юзкейсов).

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

sab123 June 14th, 2013
Функциональное программирование и корректность - это вещи несмешивающиеся :-)

_windwalker_ June 14th, 2013
и сколько мегабаксов сударь уже заработал ?

на первом я подпишусь под идеи.

akuklev June 15th, 2013
Я не бизнесмен.

vit_r June 14th, 2013
И за 50 лет эту возможность так никто и не придумал.

"А мужики-то и не знают!"

Вообще не понятно, откуда "доказательства правильности" вылезли. Даже не представляю, как надо было читать, чтобы такое вывести.

sab123 June 14th, 2013
Дык, где? Нетути. Руками-то размахивать все горазды, а на практике оно нифига не работает.

kray_zemli June 15th, 2013
Чёт не догнал, это всё о чем вообще?

  • 1
?

Log in

No account? Create an account