0

我正在使用 SPARK Discovery 2017 中 spark_io 示例中的 SPARK.Text_IO。

我的问题是，许多 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 行“medium: precondition may fail” 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 是可读的并且它不是文件结尾？

4

1 回答 1

2

首先让我说自从特别评论的日子以来我没有使用过SPARK，所以我的回答可能无法反映当前的使用情况。

查看 SPARK 的一种方式是，它让您考虑程序可能遇到的每一件事。如果前提条件为 False，你的程序应该怎么做？你必须表明你已经考虑过这种可能性。

假设 Standard_Input 上的所有 SPARK.Ada.Text_IO 操作都有一个包括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。在某些情况下，您正在从管道或输入重定向中读取数据。如果用户在循环期间输入 EOF，则当 End_Of_File 为 True 时，您的过程可能会调用 Get_Immediate，因此 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;

然后，如果 End_Of_File 变为 True（假设 IR 的某些字段在这种情况下未通过您的一项检查），您将确定 Get_Immediate 的先决条件得到满足并具有明显期望的行为（无限循环）。

您的代码有一些令人费解的地方。首先是全局变量。全局变量是万恶之源，或者至少保证代码不可读。然后是程序的特殊性。不是更一般的东西，比如

procedure Wait_For_Key (Key : in Character);

是否同样易于编写和证明，并且更有用？然后是嵌套 if 语句的字符串，我发现它比与and then. 最后，将布尔值与 True 进行比较。由于“=”返回布尔值，这是否表明需要的是布尔值，即“=”左侧已经存在的值？

也许这意味着“=”的结果也必须与True进行比较。然后那个“=”的结果也必须与True进行比较。这可能会更好，因为它可以确保写这篇文章的人永远不会完成。

于 2017-11-17T14:45:15.547 回答