PROSAGA码农传奇-Ada-阿达：一系列任务

<div class =“post-text”itemprop =“text”>
  <P>
    这并不会导致gnatprove窒息。但我不太清楚如何证明这个循环
     <code>
      Claim
    </code>
     在
     <code>
      T
    </code>
     退出
     <code>
      Ps (J)
    </code>
     被声称（我添加了一个
     <code>
      Is_Claimed
    </code>
     功能
     <code>
      P
    </code>
    ，但无法标记它
     <code>
      Ghost
    </code>
    ，不能称它为“因为在SPARK中不允许在干扰环境中调用易失性函数”;并使其成为带有out参数的子程序没有帮助。请注意，我的SPARK技能相当小）
  </p>
   <pre>
    <code>
      protected type P is
   procedure Claim (Succeeded : out Boolean);
private
   Claimed : Boolean := False;
end P;

subtype Thread_Range is Integer range 1 .. 2;

Ps : array (Thread_Range) of P;

Ts : array (Thread_Range) of T;

task body T is
   Which : Integer;
begin
Claim:
   for J in Thread_Range loop
      declare
         Claimed : Boolean;
      begin
         Ps (J).Claim (Succeeded => Claimed);
         if Claimed then
            Which := J;
            exit Claim;
         end if;
      end;
   end loop Claim;

loop  -- having a loop keeps gnatprove quiet
      delay until Ada.Real_Time.Time_Last;
   end loop;
end T;

protected body P is
   procedure Claim (Succeeded : out Boolean) is
   begin
      if not Claimed then
         Claimed := True;
         Succeeded := True;
      else
         Succeeded := False;
      end if;
   end Claim;
end P;

</code>
  </pre>
</DIV>