From: Optikos <optikos@verizon.net>
Subject: Re: SPARK prooving an array of Positives.
Date: Thu, 1 Aug 2019 17:02:41 -0700 (PDT)
Date: 2019-08-01T17:02:41-07:00 [thread overview]
Message-ID: <6b8f72b9-27f1-4590-896f-173b7a540a14@googlegroups.com> (raw)
In-Reply-To: <28e4ac2e-311b-40c4-ad81-42f55129ccd1@googlegroups.com>
On Tuesday, July 30, 2019 at 11:35:54 AM UTC-5, 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;
As per the Axis_Value restriction to 32-bit modular-arithmetic integer portion of Brad Moore's more elaborate rewrite in his reply, the when-2 clause in Shark8's version could pessimistically be construed to be as much as a 128-bit integer when multiplying two Interfaces.Unsigned_64 modular-arithmetic integers together. I suspect that that overt revelation to SPARK regarding 32-bit multiplicands is the main corrective act among Brad Moore's multiple edits. I do admire how SPARK automatedly figured out (apparently via term replacement) in Brad Moore's variant that
> when 2 => return Result_Value (First) * Result_Value (Last);
could be rewritten equivalently as
when 2 => return Result_Value (First * Last);
in order to make obvious the logical deduction of lack-of-overflow-of-64-bit-unsigneds-due-to-multiplying-two-mere-32-bit-unsigneds possible in this proof.
> 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?)
prev parent reply other threads:[~2019-08-02 0:02 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
2019-07-31 4:20 ` Brad Moore
2019-08-02 19:16 ` Shark8
2019-08-02 0:02 ` Optikos [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox