Создание пакета не на библиотечном уровне в SPARK Ada

Question

Как создать экземпляр не-библиотечного уровня в SPARK Ada?

Скажем, у меня есть что-то вроде:

subtype Die is Integer range 1..6;
package Random_Die
is
  new Ada.Numerics.Discrete_Random(Die);

Это дает мне ошибки:

instantiation error at a-nudira.ads.45
incorrect placement of "Spark_Mode"
Random_Die is not a libray level package

Предположительно мне нужно отключить SPARK_Mode для Ada.Numerics.Discrete_Random, но я не могу найти правильное место для размещения прагмы.

Answer 1

Сообщение не так много о Ada.Numerics.Discrete_Random, Spark-2014 хочет, чтобы вы сделали свой безымянный пакет, Unnamedскажем, чтобы быть на уровне библиотеки, как упоминает Джейкоб Спарре Андерсен в своем ответе. Для остроумия:

with Ada.Numerics.Discrete_Random;

--procedure Outer is
   package Unnamed
      with Spark_Mode => On
   is
      subtype Die is Integer range 1..6;
      package Random_Die
      is
        new Ada.Numerics.Discrete_Random(Die);
   end Unnamed;
--begin
--   null;
--end Outer;

Удаление переносов комментариев и перевод Outer выдает ваше сообщение об ошибке. Идет перевод Unnamed как будет хорошо работать, и gnatprove не имеет претензий Другими словами, Unnamed затем пакет уровня библиотеки. В Outer это не так, и это заставляет GNAT выдавать диагностическое сообщение.

Answer 2

Обобщения проверяются только SPARK, когда они создаются.:-(

Сообщение об ошибке выглядит так, как будто вы пытались поместить аспект SPARK_Mode где-то внутри универсального. Это не будет работать. Вы должны поставить SPARK_Mode => On аспект на единицу создания экземпляра универсального пакета.