Нет глобального контракта для процедуры / функции

Question

У меня есть процедура в модуле SPARK, которая вызывает стандарт Ada-Text_IO.Put_Line,

Во время проверки я получаю следующее предупреждение warning: no Global contract available for "Put_Line",

Я уже знаю, как добавить соответствующий контракт зависимости данных к процедурам и функциям, написанным мной, но как мне добавить их к процедурам / функциям, написанным другими, где я не могу редактировать исходные файлы?

Я просмотрел разделы 5.2 и 7.4 руководства пользователя Adacore SPARK 2014, но не нашел пример решения моей проблемы.

Answer 1

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

Есть два способа передать недостающую информацию:

1. Верификатор может проверить исходный код функции. Затем он может попытаться создать глобальные контракты сам.
2. глобальные контракты указаны явно, см. RM 6.1.4 ( http://docs.adacore.com/spark2014-docs/html/lrm/subprograms.html)

В этом случае вызываемая вами процедура является частью системы времени выполнения (RTS), и, следовательно, источник не виден, и вы, вероятно, не можете / не должны его изменять.

Что делать на практике?

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

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

Если вы не так серьезно относитесь к результатам, то вы можете рассматривать это как предупреждение, с которым вы могли бы жить.

Answer 2

Пакеты Wrapper для использования при разработке приложений SPARK можно найти здесь: https://github.com/joakim-strandberg/aida_2012

Answer 3

Я думаю, что вы просто не можете добавлять контракты Spark на код, который вам не принадлежит, особенно код из стандарта Ada.

Что касается Text_Io, я нашел кое- что, что может быть полезным для вас в справочном руководстве.

РЕДАКТИРОВАТЬ

Еще одно решение по сравнению с тем, что сказал Мартин, согласно книге "Создание приложений с высокой степенью целостности с помощью Spark", заключается в создании пакета-оболочки.

Поскольку Spark требует от вас работы с пакетами Spark, но позволяет вам зависеть от спецификации Spark с телом Ada, решение заключается в создании пакета Spark, охватывающего ваши вызовы Ada.Text_io.

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