在SPARK中将索引任务链接到相应的索引受保护类型的好方法是什么?
有关细节,请考虑以下设置:
子类型Thread_Range是自然范围1..n;受保护的P型……
这并不会导致gnatprove窒息。但我不太清楚如何证明这个循环 Claim 在 T 退出 Ps (J) 被声称(我添加了一个 Is_Claimed 功能 P ,但无法标记它 Ghost ,不能称它为“因为在SPARK中不允许在干扰环境中调用易失性函数”;并使其成为带有out参数的子程序没有帮助。请注意,我的SPARK技能相当小)
Claim
T
Ps (J)
Is_Claimed
P
Ghost
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;