验证循环终止

作者: 老夫的少女心
发布时间: 2024-04-18 04:13:17 (2天前)
转自：

3 条回复

0#
回复此人
小鬼 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 我将使用有界循环结构（for循环）迭代数组。 for循环更容易处理数组边界和空数组。这适用于我在GNAT CE 2018（在这里使用SPARK 2014）： </p> <pre> <code> package Foo with SPARK_Mode => On is type MyArray is array (Integer range <>) of Integer; procedure Find (Key : in Integer; Data : in MyArray; Index : out Integer; Found : out Boolean) with Post => (if Found then Data (Index) = Key); end Foo; </code> </pre> <P> 和 </p> <pre> <code> package body Foo with SPARK_Mode => On is ---------- -- Find -- ---------- procedure Find (Key : in Integer; Data : in MyArray; Index : out Integer; Found : out Boolean) is begin Found := False; Index := Data'First; for I in Data'Range loop if Data (I) = Key then Found := True; Index := I; end if; pragma Loop_Invariant (Index in Data'Range); pragma Loop_Invariant (if Found then Data (Index) = Key else Data (Index) /= Key); exit when Found; end loop; end Find; end Foo; </code> </pre> </DIV>

编辑
1#
回复此人
大魔王 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 如果我用典型的Ada成语写这个，我得到 </p> <pre> <code> package SPARK_Proof is type Integer_List is array (Positive range <>) of Integer; type Find_Result (Found : Boolean := False) is record case Found is when False => null; when True => Index : Positive; end case; end record; function Match_Index (Value : Integer; List : Integer_List) return Find_Result; end SPARK_Proof; package body SPARK_Proof is function Match_Index (Value : Integer; List : Integer_List) return Find_Result is -- Empty begin -- Match_Index Search : for I in List'Range loop if Value = List (I) then return (Found => True, Index => I); end if; end loop Search; return (Found => False); end Match_Index; end SPARK_Proof; </code> </pre> <P> 这更短更清晰。我不知道用SPARK证明是否更容易。 </p> </DIV>

编辑

登录后才能参与评论