Как доказать, что предварительное условие процедуры SPARK.Text_IO будет выполнено

Question

Я использую SPARK.Text_IO из примера spark_io в SPARK Discovery 2017.

Моя проблема в том, что многие из процедур SPARK.Text_IO имеют предварительное условие, что я не знаю, как начать пытаться доказать именно то, что стандартный ввод читаем, а мы не в конце файла. Моя попытка, как показано в приведенном ниже коде, состояла в том, чтобы добавить предварительное условие процедуры SPARK.Text_IO (в данном случае Get_Immediate) к предварительному условию вызывающей процедуры, полагая, что, возможно, это гарантирует доказателю, что это предварительное условие будет истинным, Это не сработало. Вот пример того, о чем я говорю:

Тестовая спецификация:

with SPARK.Ada.Text_IO; use SPARK.Ada.Text_IO;

package test with SPARK_Mode
is

   continue_messages_key : Character := ' ';

   procedure User_Wait_For_Continue_Messages_Key
   with Global => (In_Out => Standard_Input,
                   Input => continue_messages_key),
        Pre => Is_Readable (Standard_Input) and then
                    not End_Of_File; 

end test;

Тестовое тело:

pragma SPARK_Mode(On);

package body test is

   procedure User_Wait_For_Continue_Messages_Key
   is
      IR : Immediate_Result;
      Avail : Boolean;
   begin
      loop
         Get_Immediate(IR, Avail);
         if Avail then
            if IR.Status = Success then
               if IR.Available = True then
                  if IR.Item = continue_messages_key then
                     return;
                  end if;
               end if;
            end if;
         end if;
      end loop;
   end User_Wait_For_Continue_Messages_Key;

end test;

Ошибка, которую дает проверяющий, находится в строке Get_Immediate "средний: предварительное условие может завершиться с ошибкой". Прототип и контракт процедуры Get_Immediate приведены ниже:

procedure Get_Immediate (Item      :    out Character_Result)
     with Global => (In_Out => Standard_Input),
          Pre    => Is_Readable (Standard_Input) and then
                    not End_Of_File,
          Post   => Is_Readable (Standard_Input) and
                    Name (Standard_Input) = Name (Standard_Input)'Old and
                    Form (Standard_Input) = Form (Standard_Input)'Old and
                    Is_Standard_Input (Standard_Input);

Как вы докажете SPARK, что Standard_Input доступен для чтения и что это не конец файла?

Answer 1

Позвольте мне начать с того, что я не использовал SPARK со времени специальных комментариев, поэтому мой ответ может не отражать текущее использование.

Один из способов взглянуть на SPARK состоит в том, что он заставляет вас думать обо всем, с чем может столкнуться ваша программа. Что должна делать ваша программа, если предварительным условием является False? Вы должны показать, что вы рассматривали эту возможность.

Предполагая, что все операции SPARK.Ada.Text_IO для Standard_Input имеют постусловие, включая Is_Readable (Standard_Input) как это делает Get_Immediate, тогда достаточно поставить что-то вроде

pragma Assert (Is_Readable (Standard_Input) );

в начале вашей программы и добавьте это в постусловие вашей процедуры (и любые другие подпрограммы, которые у вас есть, которые читают Standard_Input). Тогда вы должны быть уверены, что эта часть предварительного условия выполняется во всей вашей программе. (Утверждение может не понадобиться, если SPARK изначально гарантирует, что Standard_Input доступен для чтения.)

not End_Of_File немного сложнее. Возможно, это будет False, по крайней мере, на некоторых платформах. Linux, например, обрабатывает Ctrl-D как EOF, когда вводится первым в строке. Также есть случаи, когда вы читаете из канала или перенаправления ввода. Ваша процедура может вызвать Get_Immediate, когда End_Of_File равен True, если пользователь вводит EOF во время цикла, поэтому неудивительно, что SPARK не может доказать обратное. Вероятно, вам нужно снять эту часть с предварительных условий вашей процедуры и изменить свое тело на что-то вроде

All_Chars : loop
   if not End_Of_File then
      Get_Immediate (IR, Avail);

      exit All_Chars when Avail               and then
                          IR.Status = Success and then
                          IR.Available        and then
                          IR.Item = Continue_Messages_Key;
   end if;
end loop All_Chars;

Тогда вы будете уверены, что предварительное условие Get_Immediate выполнено и будет иметь желаемое поведение (бесконечный цикл), если End_Of_File станет True (при условии, что какое-то поле IR не выполнит одну из ваших проверок в этом случае).

В вашем коде есть некоторые загадочные вещи. Во-первых, это глобальная переменная. Глобальные переменные являются корнем зла или, по крайней мере, гарантируют нечитаемый код. Тогда есть специфика процедуры. Не было бы что-то более общее, как

procedure Wait_For_Key (Key : in Character);

быть таким же простым, чтобы написать и доказать, и более полезным? Тогда есть строка вложенных операторов if, которые мне труднее читать, чем эквивалентные условия, связанные с and then, Наконец, есть сравнение логического значения с истинным. Поскольку "=" возвращает логическое значение, не означает ли это, что для этого требуется логическое значение, то есть то, что уже находится в левой части "="?

Возможно, это означает, что результат "=" также следует сравнивать с True. Тогда результат этого "=" также должен сравниваться с Истиной. Это может быть лучше, так как это гарантирует, что тот, кто пишет, никогда не закончит.