From: Shark8 <onewingedshark@gmail.com>
Subject: SPARK prooving an array of Positives.
Date: Tue, 30 Jul 2019 09:35:52 -0700 (PDT)
Date: 2019-07-30T09:35:52-07:00 [thread overview]
Message-ID: <28e4ac2e-311b-40c4-ad81-42f55129ccd1@googlegroups.com> (raw)
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?)
next reply other threads:[~2019-07-30 16:35 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-07-30 16:35 Shark8 [this message]
2019-07-31 0:18 ` SPARK prooving an array of Positives Anh Vo
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