Несколько лет назад было обсуждение:
> -- AVC писал(а):
> Спасибо за ссылку на SPARK.Интересно также насчёт "самописного" верификационного инструментария (хотя не вполне ясно, что он из себя представляет).
Как я понимаю, по поводу "самописного" верификационного инструментария имеется в виде механизм виртуального текста из языка Anna для Ada или похожий механизм абстрактных функций из SPARK.
Суть в том, что можно описывать свой функции, которые нужны только для верификации программы (для формальной или же run-time) и не требуются для работы самой программы. Например, в программе, которая работает с сбалансированным AVL деревом можно написать функцию, которая проверяет сбалансированность дерева. И использовать эти функции в утверждениях в различных местах программы. То есть, если, например, Unit Test рассматривают функции программы как черные ящики и проверяют их на конкретных входных значениях и проверяется совпадают ли выходные значения. То виртуальный текст из Ada помогает проверять свойства программы, например, что дерево сбалансировано, массив отсортирован и т.д.. Таким образом получается self-checking программа. Это довольно таки интересная идея, похоже она получила развитие только в области языка программирования Ada.
Как думаете, будет ли полезен подобный механизм виртуального текста для языка Оберон?