DRAKON.SU

Да, ТЗ, ТП, РП - обычные аббревиатуры...
Я пытаюсь все-таки как-то наших студентов на тему выступления раскочегарить.
Вот в понедельник начинаем Коде ревью по курсовым со 2 курсом.
Но большинство из них все-таки интроверты, поэтому пока трудно идет.

Владимир Шелехов,
Что нибудь еще содержательное в темах "Формальные методы. Ликбез" и "Инженерия требований. Ликбез" будет?

Без предъявления претензий от специалистов по формальным методам к остальным (ковыряющим) программистам:
http://forum.oberoncore.ru/viewtopic.php?p=94204#p94204 от Суббота, 05 Декабрь, 2015 13:44

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

Приведу пример методики с форума: http://forum.oberoncore.ru/viewtopic.php?p=35027#p35027 от 27.09.2009, стиль Скульптор, предложил Геннадий Тышов, он же предложил ИС Дракон.

Извините, что пока нет возможности полноценно участвовать в Форуме. Надеюсь, в ближайшее время дать по одной лекции в каждом ликбезе.

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

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

Это разговор о технологии программирования. Но об этом не сейчас и не здесь.

Пример:
Если я запускаю Linux, после модификации драйвера FB (Графического буфера) и вижу что ядро выдаёт Опс сообщение на этапе загрузки файловой системы. То я не делаю вывод что проблема с FS (Файловой системы) исходя из содержания стека вызова функции на которой ядро свалилось.

Зная ядро, что у меня стартуют параллельно несколько модулей именно в этот момент (в зависимости они собраны внутри ядра или подгружаются), я сразу могу сказать конкретно какие 3 из них в этом момент работают (в этом моменте и проявляется знание спецификации - точно знать что за чем стартует и что конкретно меняет). Надо сказать что в этот момент лог не доступен, а printk изменяют время старта и не всегда помогали в версиях ядра Linux ~2.1.

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

http://forum.oberoncore.ru/viewtopic.php?p=94219#p94219
Это всего лишь констатация того факта, что каждый занимается своим делом.

"Элитный специалист по формальным методам" не будет востребован там, где от программиста требуется знание прикладной области.
Нужно еще уметь формулировать функциональные требования к создаваемому ПО.

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

Ваши высказывания вызывают тёплое чувство понимания.

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

Проект должен быть достаточно большой, чтобы такие накладные расходы не превратились в гирю на шее.

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

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

При этом подходе за проект отвечает Тим-лидер/проджект-лидер, за качество процесса создания кода специалист из PPMG (проект-менеджер), а за функционал конечного продукта специлист из HQ (главного офиса).

Test-driven design -- по смыслу можно увидеть некое родство и некую смежность с формальными спецификациями.

Генераторы тестов с максимумом стохастики и автоматической проверяемостью -- отличное дело.

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

(Если мозг правильно соображает, в чём нет полной уверенности в сей момент.)

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

Про генераторы тестов показалось интересным. Что они должны делать? Исходя из предусловий и постусловий задавать входные данные и проверять выходные? В таком случае, можно будет тестировать код просто передавая модуль на вход такого генератора (естественно не все возможные значения, но хоть какую-то их часть)? А если еще и верификацию сюда прикрутить (хотя бы в том плане, что из предусловий следуют постусловия, то ваще сказка.

Ссылочка в тему: http://citforum.ru/SE/quality/fm_rethinking/

По поводу статьи цитата: "Ни одна из имеющихся методов не может в этой ситуации обеспечить полную и точную информацию."

Я приводил тут классификацию функциональных уровней. Каждая функция относиться к одному из уровней.
Если функция занимает 2 уровня - пожелание её разделить на 2 разных функции/процедуры.
Если занимает 3 уровня - настоятельное пожелание к программистам.
Если более одной функции можно отнести сразу к 4 различным уровням - это порождает сильные вопросы по поводу квалификации автора.

Методика опробована на реальном проекте. Так же после применения этой методики был использован один из лучших динамических анализаторов кода. Совпадения в 75-80% случаев.

А именно из 200 функций методикой выделено 8 функций. Из которых в 6 динамическим анализатором кода были найдены ошибки (динамический анализатор нашёл мелкие замечания по ещё 2 функциям, которые не входили в мой список, но вызывались функциями из моего списка). Попутно была получена статистика по отладочным сообщениям (20% функций их имела). И формальным проверкам входных и выходных значений каждой функции/процедуры (пост- и предусловия) в коде (по моему было менее 30%).

Это при том что в проекте переписанном пионерами с нуля в цейпноте (писать это не читать), была напрочь отвергнута модель бывшего тим-лидера (который к тому времени был ушлан командой и благополучно нашёл работу в более серьёзной компании), но новой модели создано не было (старая модель была не понята так как опиралась на 20 патентов минимум - пионерам сложно всё это понять). Пионеры плясали от тестов из HQ.

В данной статье мало конкретики, а многие утверждения довольно спорны.

Дэвид Парнас -- легендарная личность.
Он является автором концепции абстрактных типов данных, чрезвычайно популярной в 1980-ых гг. в нашем Новосибирском филиале Института Точной Механики и Вычислительной Техники.

Всем известный набивший оскомину пример: абстрактный тип данных "стек". Аксиомы стека. Абстрактный тип данных "стек" как новая математическая сущность. Попытки создания "новой" математики последователями концепции, понятно, ни к чему не привели. Большое число "примеров" абстрактных типов, в которых кругом торчат императивные "уши". Здесь удивляет другое. Почему никто не сказал, что аксиомы стека -- это глупость. Есть аксиомы натуральных чисел, из которых и следуют все свойства стека, а аксиом стека просто не должно быть. Это классический пример того, что подавляющее большинство людей внушаемы, не только простых людей, но и принадлежащих научному сообществу. Впрочем, вера в науке -- интересная, но другая тема.

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

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

В чем Д.Парнас безусловно прав, это то, что формальные методы практически не применяются в производственном программировании, их доля в мире менее процента. Это было подтверждено и на одном из обзорных пленарных докладов по истории формальных методов, посвященных сорокалетию формальных методов. Здесь необходимо уточнение: все же речь идет о сильных формальных методах, таких как дедуктивная верификация. Например, статические верификаторы (см. лекцию 2) наверняка используются более чем в 10% случаев. Но их применять могут все, не только специалисты по формальным методам, хотя лишь специалисты способны хорошо написать assert'ы.

Подчеркнем, что Дэвид Парнас не против формальных методов. Он лишь предлагает пересмотреть их основы, утверждает, что нет прогресса. А где он есть? Во всей мировой науке Computer Science ступор по меньшей мере последние 20 лет.

Д. Парнас не единственный, кто критикует формальные методы. Академик Виктор Иванников ранее говорил о бесполезности дедуктивной верификации. Однако продолжал учить дедуктивной верификации своих студентов в МГУ. Года три-четыре назад В.П. Иванников изменил свою точку зрения. Дедуктивная верификация применяется для модулей ядра ОС Linux. Совсем недавно профессор Андрей Терехов из Питера, внедривший международный образовательный стандарт по Программной инженерии в Российском университетском образовании, сказал, что формальные методы -- это хе..ня. Наверное, он не стал бы бросаться такими словами, если бы почитал зарубежные работы или хотя бы познакомился с работами своих коллег из ИСП РАН. Впрочем, подобные суждения провоцирует слабость наших работ по формальным методам.

Есть другие причины неприменения формальных методов в практическом программировании.
Это неумение программистов писать формальные спецификации. Данная проблема была затронута в одном из сообщений. Формальным методам учат только в ведущих мировых университетах. Инженеры-верификаторы -- это уровень PhD (кандидатской диссертации). Понятно, что таких немного. А специально систематически, писать формальные спецификации в мире больше нигде не учат. А надо бы.

Квадратные уравнения когда-то давно тоже только великие учёные умели решать, а сейчас каждый школьник может. Также и с верификацией будет.

Подозреваю, что здесь имелось ввиду нечто другое - модули. Абстрактные т.д. - это , наверное, всё же с Б.Лисков больше связаны.

Да нет, Д.Парнас написал главную свою работу по упрятыванию данных в 1972г., а публикации Барабары Лисков по языку CLU начинаются с 1974г. В начале 1980-х имя Б.Лисков в СССР еще не звучало.

А основной результат Барбары -- принцип подстановки для спецификации наследуемых методов. Когда я на него сослался в своей статье, то Бертранд Мейер, увидев мою ссылку, сказал мне, что он ее опередил.

Вот несколько ссылок. (Исключительно в целях верификации фактов

Работа Лисков с соавтором, цитируемая в контексте абстрактных типов данных:
"Programming with Abstract Data Types" Barbara Liskov and Stephen Zilles, 1974
http://web.cs.iastate.edu/~hridesh/teac ... liskov.pdf

В ней есть ссылка на:
INFORMATION DISTRIBUTION ASPECTS OF DESIGN METHODOLOGY *. D.L. PARNAS, 1972
https://cseweb.ucsd.edu/~wgg/CSE218/Par ... bution.PDF

А вот то, на что часто ссылаются, когда речь идёт о модулях.
David Parnas
"On the Criteria to be Used in Decomposing Systems into Modules."
Communications of the ACM, Vol. 15, No. 12,
December 1972. pp. 1053 – 1058.
https://www.cs.umd.edu/class/spring2003 ... iteria.pdf

PS.
Если подойти формально, то можно подсчитать в каких работах больше встречается "abstract", а в каких - "module"

PPS.
И, опять же, Дейкстра, 1969 г.
...
'4. Abstract data structures.'
...
в http://www.cs.utexas.edu/users/EWD/tran ... WD268.html

Можно, наверное, ещё нарыть плодов коллективного разума

Если ближе к практике:

Drakon editor хранит данные в SQLite.
По методологии, которую я использую, скрипты разбирают код и хранят в MySQL (Прикладываю презентации того что уже сделано).

Между этими двумя базами можно конвертировать дампы в обе стороны.
http://gist.github.com/esperlu/943776
http://www.redmine.org/boards/2/topics/12793?r=24983

Функциональные уровни (пока) я назначаю вручную в базе данных, после просмотра кода.
Но пользуюсь вполне формализуемыми правилами, которые можно автоматизировать:

Так например оператор CASE или структура Шампура в Drakon относятся к состояниям конечного автомата.
Условия в операторе IF к переключателю памяти или пересылке между отдельными устройствами.
Блоки операторов (BEGIN..END, {}) внутри IF, если они используют регулярные выражения или фильтры (построенные на базе IF так же) относятся к уровню компилятора/парсинга.


Более того из Drakon editor возможен экспорт в различные скрипты и языки. В Verilog в том числе. Главное правильно выбрать из базы данных структуры, которые хотелось бы разместить в логике ПЛИС. Понятно что тут надо использовать готовые блоки/структуры для DMA, регистров, АЛУ и т.д. Но параметры для этих блоков брать с учётом размещаемого программного кода.

Для Verilog есть логический синтезатор ABC, который делает размещение логики на FPGA (ПЛИС).

Прослеживается методология: Мета-программирование на уровне баз данных и Drakon editor, и далее спуск до архитектуры микропроцессора.

https://github.com/espressif/ESP32_RTOS_SDK

Вот действительно RTOS с этим SDK и новым чипом обещает стать народным. Прошу обратить внимание на эту SoC. Это к вопросу о режиме реального времени и таймерам.

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

https://github.com/DuinOS/FreeRTOS/blob ... e/timers.c

https://www.youtube.com/watch?v=HCGHb0OVz1s