kdvГоспода, есть у кого что сказать по этому поводу?
Я имею в виду, практическое применение вот этих волшебных слов на предприятии.

Чтобы было понятно, о чем я спрашиваю, вот ссылка
http://www.ict.edu.ru/ft/005645/62322e1-st09.pdf
"Методы верификации программного обеспечения"

p.s. я считаю, что это в целом очередное словоблудие. А вот на некоторых предприятиях для начальников ИТ это уже головная боль, в том смысле, что сверху по голове стучат этой верификацией, а как это правильно оформляется - х.з.
Документ хороший. Годный. Несколько улыбнула отсылка к Rational Rose но в целом ок.
О чем это все. Всё я нечитал. Нет времени и по диагонали.

Очень часто кастомер сам требует подключения внешних инструментов верификации.
В основном это требования Security и Compliance. Для банковского аутсорсинга
это требование. Часто issue от SonarQube или Veracode класса security имеет
статус блокера и требует срочного решения.

Поэтому вопрос - "что есть сказать" это вопрос вчерашнего дня. Вопрос
сегодняшний - это как это использовать. И как правильно использовать
с выгодой для себя.

Basil A. SidorovmaytonВ основном это требования Security и Compliance.
Для банковского аутсорсинга это требование.
Часто issue от SonarQube или Veracode класса security имеет статус блокера и требует срочного решения.При всём уважении, но, наверное, статус такой не потому, что эти инструменты делали клёвые парни, а потому, что эти инструменты соответствуют каким-то спецификация каких-нибудь PCI-DSS (или как их там) и, весьма вероятно, прошли требуемую сертификацию?
1) Не только карточных продуктов но и банковской деятельности в целом. Это ведь не только карточки.
2) Насчет конкретных ISO и прочих документов я точно не скажу. Надо искать. Скорее всего ISO содержит
общие слова касающиеся организации процессов. А Sonar и Veracode - это уже конкретные программные продукты
которые где-то в стеке разработки решают какой-то один пункт из организации процессов.

Речь идёт не о толке а скорее о минимизации рисков.

kealon(Ruslan)tip78почитайте лучше это: 10 правил, которые позволяют NASA писать миллионы строк кода с минимальными ошибками улыбнуло, в таких рамках умрёт практически любой кровавый интерпрайз
Я-бы откоментил некоторые выдержки.
Нужно сильно ограничивать ветвления и условия. Не использовать goto, setjmp или longjmp, не использовать прямую или косвенную рекурсию.
Я привык использовать рекурсию при работе с файловой системой и древовидными
структурами данных.

Не совсем понятно как можно не использовать рекурсию. Возможножно NASA подразумевает под
этим некий узкий круг задач. А если трансформировать рекурсию в FSM с очередью (Queue)
то вряд-ли это увеличит надежность ПО. Ну .. с точки зрения цены сопровождения такого кода.
Любая функция должна уместиться на одном стандартном листе бумаги, одно выражение на строку и одна строка на определение. Обычно это означает, что функция не должна быть длиннее 60 строк.
60 строк для чего? Ассемблер что-ли? Я-бы уменьшил до 7-14 строк если речь идет о ЯВУ.

Должно быть не более двух ассертов на функцию. Ассерты используются для проверки аномальных условий, которые не могут произойти при реальном запуске. Ассерты не должны содержать сайд-эффектов, и по формату должны быть Boolean-тестами. Когда ассерт падает, должно запуститься специальное действие по восстановлению, например, возврат условия падения обратно в вызывающую функцию. Если проверяющая программа доказывает, что ассерт никогда не фейлится или никогда не удовлетворяется, то правило считается нарушенным. (Нельзя обойти это правило с помощью бессмысленных “assert(true)”).

Здесь - непонятно. Если ассерт никогда не фейлится то я считаю что все ОК и оставляю его в покое.
Пускай себе будет в отладочной версии кода. Или в тексте не совсем корректный перевод.
Использование указателей должно быть ограничено. Допустимо не больше одного уровня разыменования. Операторы разыменования не должны быть скрыты в макро определениях или внутри typedef. Указатели на функции запрещены.

Почему указатели не функции запрещены? Это полезный механизм полиморфизма. Или они его
принципиально не используют? На что заменяют? (Речь идет о Си).

unregesteredSiemarglГлавное - в доказательства правильности алгоритмов не влезть =)

Прочитайте Дейкстру он как раз очень любил доказывать правильность программ.
Можно в комментариях прописать инварианты циклов, входные и выходные параметры. Если всё аккуратно сделать - вот оно и доказательство )
Я думаю что между кодом и каментом будет некая.. Натяжка :)