DRAKON.SU
https://forum.drakon.su/

Дискуссия по формальным методам и инженерии требований
https://forum.drakon.su/viewtopic.php?f=140&t=5581
Страница 1 из 4

Автор:  Владимир Шелехов [ Пятница, 27 Ноябрь, 2015 20:03 ]
Заголовок сообщения:  Дискуссия по формальным методам и инженерии требований

Если хочется отвести душу и побузить, сказать что-нибудь хорошее или не очень и не обязательно по теме, и при этом нет желания заводить новую тему, то Вам сюда

Автор:  ilovb [ Пятница, 27 Ноябрь, 2015 20:54 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

А вы сюда отвечать то будете?
Создали две темы, а на диалог не идете.

Автор:  adva [ Суббота, 28 Ноябрь, 2015 10:15 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Не совсем по теме:
Хотел бы узнать, кто какие методологии разработки использует? И какие плюсы/минусы видите.
До сих пор работал в не очень крупных конторах, в которых как таковых методологий никаких не использовалось (ну или я не увидел чего). Т.к. в основном задачи были сравнительно мелкие и более по сопровождению, а не по разработке, то вполне без них обходились. Но сейчас хотел бы выйти в этом вопросе на новый уровень (для чего возможно и место работы попробую сменить, чтобы было где опыта набраться, ну или еще какое решение придумаю). Как успел пообщаться с одной вроде бы серьезной в этом плане конторой, они используют гибкую методологию (конкретно скрам, или как он там). Ранее я как-то ненадолго сталкивался с такой системой (не скрам вроде бы, но какая-то из гибких методологий), но мне показалось, что в таком методологии производятся скорее некачественные решения, которые также достаточно сложно поддерживать. Кто что может сказать по этому поводу?

Автор:  ilovb [ Суббота, 28 Ноябрь, 2015 13:19 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

adva писал(а):
Хотел бы узнать, кто какие методологии разработки использует?

Мы никакие не используем. Пытались, но не взлетело. Своим программистам я просто регулярно промываю мозг на темы понимания постановки, понимания задачи, решения задачи, как писать понятно для коллег, что делать со сложными задачами и т.д. и т.п. Эффект есть, но многие вещи мы так и не научились делать.
Самая главная беда - это ТЗ.

Изображение

Автор:  ignat99 [ Суббота, 28 Ноябрь, 2015 19:18 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

adva писал(а):
Не совсем по теме:
Хотел бы узнать, кто какие методологии разработки использует? И какие плюсы/минусы видите.
До сих пор работал в не очень крупных конторах, в которых как таковых методологий никаких не использовалось (ну или я не увидел чего). Т.к. в основном задачи были сравнительно мелкие и более по сопровождению, а не по разработке, то вполне без них обходились. Но сейчас хотел бы выйти в этом вопросе на новый уровень (для чего возможно и место работы попробую сменить, чтобы было где опыта набраться, ну или еще какое решение придумаю). Как успел пообщаться с одной вроде бы серьезной в этом плане конторой, они используют гибкую методологию (конкретно скрам, или как он там). Ранее я как-то ненадолго сталкивался с такой системой (не скрам вроде бы, но какая-то из гибких методологий), но мне показалось, что в таком методологии производятся скорее некачественные решения, которые также достаточно сложно поддерживать. Кто что может сказать по этому поводу?


Вы говорите про методологии психологического давления/развития на/для подчинённых.

А если говорить про анализ качества кода то:

Одним статическим анализатором не обойтись, нужен динамический.
Так же для скриптовых языков JS, Python, Ruby, Perl есть статические анализаторы кода и стиля.

Сейчас даже компиляцию люди запускают в облоках, а заодно и тесты.
https://travis-ci.org/OpenBazaar/OpenBa ... s/35491781

Klocwork - кажется давно в облаке.

ncc (бесплатно, строит Call граф),
Coverity prevent,
pmccabe (бесплатно),
klocwork (то что нужно, но за деньги),

Rhapsody (это модель, это правильно но надо делать с начала проекта)

http://docs.pylint.org/run.html (статический анализатор кода для Python)

http://alternativeto.net/software/resharper/
Memory Test (DUMA/DML/VALGRIND)

А так же специальные тесты которые делает программист заказчика. Обычно их сотни, и фактически они и задают ТЗ.
Так же есть методология работы корпорации Самсунг Электроникс, за которой следит группа Проект Проджект Менеджеров в SMRC и HQ (я являюсь экспертом (4 ранг в SE) этой группы, а так же группы по Тайзен/Андроид) , основанная на строгой последовательности в работе над проектом с очередными этапами, полным документированием и отчётами. Информация об этой технологии не является открытой. Но то что указано выше - открытые инструменты, которые используются в процессе выпуска промышленного кода.

В последнее время входит в моду формальная верификация на основании модели.

1. Модель это по сути формальное описание активности всей программы. Вот на этот аргумент и надо напирать при спорах о достоинствах Актив Оберона.

2. Юнит-тестирование ( Модульное тестирование встронно в Aктив Оберон - пример: http://lists.inf.ethz.ch/pipermail/ober ... 07998.html )

Автор:  adva [ Воскресенье, 29 Ноябрь, 2015 09:14 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

ilovb писал(а):
Пытались, но не взлетело...
Самая главная беда - это ТЗ.


Думал это просто мне не посчастливилось, но похоже много где так.

А почему не взлетело не анализировали?

Тестирование тоже на пользователей возложено?

Автор:  adva [ Воскресенье, 29 Ноябрь, 2015 09:31 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

ignat99 писал(а):
А если говорить про анализ качества кода то:

Спасибо за инфу, но думаю инструменты анализа для кода 1С еще не скоро появятся. Если только самим реализовать (но лично я до этого уровня не дорос).

Автор:  ignat99 [ Воскресенье, 29 Ноябрь, 2015 14:53 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

adva писал(а):
ignat99 писал(а):
А если говорить про анализ качества кода то:

Спасибо за инфу, но думаю инструменты анализа для кода 1С еще не скоро появятся. Если только самим реализовать (но лично я до этого уровня не дорос).


http://sage.com.ua/ru.shtml?e6l0

Вот из этих диаграмм ДРАКОНА можно получить код на Обероне, можно (в теории, это похоже на спецификацию для профессионального RTL дизайнера, можно сделать логический синтез для FPGA непосредственно минут за 30).

Начальник одного из отделов программистов в 1C (не знаю точно его должности сейчас), мой товарищ. Бывший паскалист. Если вы точно сформулируете что за инструменты вам нужны, я могу переслать ему ваше сообщение. Возможно он то же не дорос пока до инструментов анализа, но может кто нибудь из его команды в этом разбирается.

Автор:  Валерий Лаптев [ Воскресенье, 29 Ноябрь, 2015 18:26 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

ilovb писал(а):
adva писал(а):
Хотел бы узнать, кто какие методологии разработки использует?

Мы никакие не используем. Пытались, но не взлетело. Своим программистам я просто регулярно промываю мозг на темы понимания постановки, понимания задачи, решения задачи, как писать понятно для коллег, что делать со сложными задачами и т.д. и т.п. Эффект есть, но многие вещи мы так и не научились делать.
Самая главная беда - это ТЗ.

Вот спасибо!
Наши студни считают, что все эти доки - это пустая трата времени. Программа жеж работает! :))
А мы - заставляем!
И ТЗ писать, И ТП писать, и рассказывать - с презентацией.

Буду посылать сюда, чтобы убедились в необходимости все это уметь в реальном программировании.

Автор:  Info21 [ Понедельник, 30 Ноябрь, 2015 18:48 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Валерий Лаптев писал(а):
Программа жеж работает! :))
А мы - заставляем!

Правильно.
Я уже 6-классникам втемяшиваю, что в программинге "жеж работает" не есть конец работы, и даже (но это более старшим), возможно, не половина.

Автор:  TAU [ Понедельник, 30 Ноябрь, 2015 21:59 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Валерий Лаптев писал(а):
И ТЗ писать, И ТП писать, и рассказывать - с презентацией.

Буду посылать сюда, чтобы убедились в необходимости все это уметь в реальном программировании.

ТП-технический проект?

C презентацией своих достижений у наших студентов обычно совсем нехорошо. Контраст очень заметен по сравнению со студентами западными. Их учат, и в итоге - сделано может быть с гулькин нос, а подано ооочень даже впечатляюще. С этим, конечно, нужно целенаправленно работать. Чтобы и на вопросы при этом умели отвечать, "защищать" работу. Очень полезно даже для собственного понимания - и иногда рождаются мысли по продолжению...

Автор:  Владимир Паронджанов [ Понедельник, 30 Ноябрь, 2015 22:16 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

TAU писал(а):
C презентацией своих достижений у наших студентов обычно совсем нехорошо.

Контраст очень заметен по сравнению со студентами западными. Их учат, и в итоге - сделано может быть с гулькин нос, а подано ооочень даже впечатляюще.

С этим, конечно, нужно целенаправленно работать. Чтобы и на вопросы при этом умели отвечать, "защищать" работу. Очень полезно даже для собственного понимания - и иногда рождаются мысли по продолжению...
Поддерживаю.

Приведу пример. Думаю и знаю, что уже некоторые студенты сделали кусовые и дипломные работы (проекты) с помощью языка ДРАКОН.

Но!

На сайте YouTube мне известно только одно видео (презентация) по языку ДРАКОН.

Причем сделана эта презентация не в России, а на Украине.

Докладчик Алена Ноздрановская, 2 курс.
Цитата:
2015 05 13 Доклад Язык Дракон
http://www.youtube.com/watch?v=ecGQLaV2oFM

Автор:  adva [ Пятница, 04 Декабрь, 2015 07:34 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

ilovb писал(а):
Пытались, но не взлетело.


А что именно пробовали? СППР от 1С не пробовали?

Автор:  Владимир Шелехов [ Суббота, 05 Декабрь, 2015 13:44 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

ilovb писал(а):
А у меня такой вопрос к коллегам:
Возможно ли на практике работать с формальными спецификациями?
Т.е., есть ли у кого реальный положительный опыт, при использовании такого подхода?
Есть. Это проект по верификации ядра операционной системы Linux. Там используются: тестирование на базе формальных спецификаций, статическая верификация, дедуктивная верификация и многое другое. В проекте 17 специалистов из Института Системного Программирования. В ИСП РАН есть и другие проекты.

Есть ли другие проекты не из ИСП? Возможно, в Питере.
В основном, проекты с использованием формальных спецификаций являются исследовательскими.
И лишь некоторые из них имеют производственную составляющую.

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

В 2006 г. я дал задание своим студентам написать предусловия и постусловия для простеньких программ.
Никто не справился.
В следующие годы я стал серьезно тренировать студентов писать формальные спецификации перед тем как дать каждому индивидуальное задание. С первого раза никто задание не сделал. Последовательно исправляя ошибки, все студенты сдали задание с 3-7 раза. Спотыкаются все: и средние, и сильные студенты; слабаков отсеяли на 1-2 курсах. И это при том, что на 1-ом и 2-ом курсах студенты изучают серьезный курс математической логики. Каждый год я удивляюсь результатам проведения индивидуальных заданий.

А может быть, формальные методы это ненужная роскошь? Нет, не роскошь.
Есть привычное заблуждение: специалисты по формальным методам всегда пишут формальные спецификации и всегда используют формальные методы. Конечно, нет. Они выступают и в роли обычных программистов. И при этом по квалификации они на порядок выше супер-программиста, ковыряющегося в отладчике.

Автор:  ignat99 [ Суббота, 05 Декабрь, 2015 14:54 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Согласен с вами полностью и по сути, мы уже начали наш проект по верификации A2. Работы будут проводиться только на нашем сервере. Проект рассчитан на длительное время. Пока же и без формальных спецификаций видны проблемы. Если чудом удаётся запустить 5-6 текстовых окошек в A2 и сохранить состояние десктопа, то при следующем запуске - лишь в 20-10% случаев удачный запуск.

Так же, считаю заслуживающими внимания материалы, статьи и инструменты по следующим ссылкам:

http://ryzhyk.net/

http://ssrg.nicta.com.au/projects/TS/drivers/synthesis/

http://ssrg.nicta.com.au/projects/TS/filesystems.pml

Автор:  Kemet [ Суббота, 05 Декабрь, 2015 15:06 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

ignat99 писал(а):
Согласен с вами полностью и по сути, мы уже начали наш проект по верификации A2. Работы будут проводиться только на нашем сервере. Проект рассчитан на длительное время. Пока же и без формальных спецификаций видны проблемы. Если чудом удаётся запустить 5-6 текстовых окошек в A2 и сохранить состояние десктопа, то при следующем запуске - лишь в 20-10% случаев удачный запуск.

Это ложь. Ни у кого, кроме ignat99 таких проблем нет

Автор:  ignat99 [ Суббота, 05 Декабрь, 2015 15:17 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Kemet писал(а):
ignat99 писал(а):
Согласен с вами полностью и по сути, мы уже начали наш проект по верификации A2. Работы будут проводиться только на нашем сервере. Проект рассчитан на длительное время. Пока же и без формальных спецификаций видны проблемы. Если чудом удаётся запустить 5-6 текстовых окошек в A2 и сохранить состояние десктопа, то при следующем запуске - лишь в 20-10% случаев удачный запуск.

Это ложь. Ни у кого, кроме ignat99 таких проблем нет


Повторяю ещё раз, я запускаю систему на Дарвине на MacBookPro, специально пересобрал на 32 бита из свежего (самого свежего репозитария).

Так же я запустил систему на Облаке с удалённым доступом на другой операционной системе. Если там будут проблемы, то я об этом напишу.
===============
Как я понял, большинство странно агрессивных людей с этого форума используют BB и запускают практически в родной среде Windows (Родной потому что Актив Оберон вырос из проекта Микрософт по портированию Оберона на .NET в 2002 году).

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

Иначе получается - врёте вы. Если из того что на вашем личном XP система работает стабильно, не следует что она работает стабильно в другом окружении. Не понимать таких элементарных вещей в 2015 году это надо очень и очень сильно быть "своеобразным".

И ещё. Если у вас запускаются 5 окон на вашем XP (которая уже не поддерживается да же MS - а об уязвимостях этой OS я писать не буду) - попробуйте их открыть на полную длиину модуля (сделать ну очень длиннымии) и напишите о результате.

Автор:  Kemet [ Суббота, 05 Декабрь, 2015 15:33 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

ещё раз - хватит нести чушь и строить из себя невесть что. мы используем разные варианты A2 - и нативные и хостовые, и я знаю о чём пишу.

Автор:  ignat99 [ Суббота, 05 Декабрь, 2015 15:37 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Kemet писал(а):
ещё раз - хватит нести чушь и строить из себя невесть что. мы используем разные варианты A2 - и нативные и хостовые, и я знаю о чём пишу.


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

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

Автор:  Пётр Кушнир [ Суббота, 05 Декабрь, 2015 16:10 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Где же, где же модераторы...

Страница 1 из 4 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/