From: Anh Vo <anhvofrcaus@gmail.com>
Subject: Re: SPARK prooving an array of Positives.
Date: Tue, 30 Jul 2019 17:18:21 -0700 (PDT)
Date: 2019-07-30T17:18:21-07:00 [thread overview]
Message-ID: <65396646-c996-4a0a-b698-3ff990467583@googlegroups.com> (raw)
In-Reply-To: <28e4ac2e-311b-40c4-ad81-42f55129ccd1@googlegroups.com>
On Tuesday, July 30, 2019 at 9:35:54 AM UTC-7, Shark8 wrote:
> I have a bit of a problem getting the SPARK provers to accept that a postcondition cannot fail. Given the following in a spec file:
>
> Type Axis_Count is range 0..999 with Size => 10;
> Type Axis_Dimensions is Array (Axis_Count range <>) of Positive
> with Default_Component_Value => 1;
> Subtype Primary_Data_Array is Axis_Dimensions(1..999);
> Subtype Random_Groups_Data is Axis_Dimensions(1..998);
>
> Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64;
>
> and the following in the implementation:
>
> Function EF( Item : FITS.Axis_Dimensions ) return Interfaces.Unsigned_64 is
> Max : Constant := Positive'Last;
> Function First return Interfaces.Unsigned_64 is
> ( Interfaces.Unsigned_64( Item( Item'First ) ) )
> with Inline, Pre => Item'Length > 0, Post => First'Result <= Max;
> Function Last return Interfaces.Unsigned_64 is
> ( Interfaces.Unsigned_64( Item( Item'Last ) ) )
> with Inline, Pre => Item'Length > 0, Post => Last'Result <= Max;
> use all type Interfaces.Unsigned_64;
> Begin
> case Item'Length is
> when 0 => return 1;
> when 1 => return First;
> when 2 => return First * Last;
> when others =>
> Declare
> Middle : Constant Axis_Count := Item'Length/2 + Item'First;
> Subtype Head is Axis_Count range Item'First..Middle;
> Subtype Tail is Axis_Count range Axis_Count'Succ(Middle)..Item'Last;
> Begin
> Return EF(Item(Head)) * EF(Item(Tail));
> End;
> end case;
> End EF;
>
> the SPARK prover is issuing warnings that the postconditions might fail.
> "medium: postcondition might fail, cannot prove First'Result <= Max (e.g. when First'Result = 0)"
> But this is impossible given that the element-type is Positive and the precondition states there is at least one element. Does anyone know why this is happening? (And how to fix it?)
Assuming you are using gnat-2019-community version, increase the level of proof by setting --level=n (n = 0 to 4) to see if it works.
Anh Vo
next prev parent reply other threads:[~2019-07-31 0:18 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-07-30 16:35 SPARK prooving an array of Positives Shark8
2019-07-31 0:18 ` Anh Vo [this message]
2019-07-31 4:20 ` Brad Moore
2019-08-02 19:16 ` Shark8
2019-08-02 0:02 ` Optikos
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox