Re: SPARK: Problem with using constants in a post annotation

[George <geo.paok@gmail.com>]

On 13 Ιαν, 13:15, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> On Jan 13, 9:26 am, George <geo.p...@gmail.com> wrote:
>
>
>
>
>
> > PLEASE IGNORE THE PREVIOUS. THE FOLLOWING IS A CORRECT VERSION OF THE
> > MESSAGE:
>
> > Hello,
>
> > I'm trying to use inside a post annotation two constants that are
> > declared in the package body. But, I can't do it, because the two
> > constants are not recognised at the point where they are used in the
> > annotation. Does anyone have an idea of how to overcome this problem?
> > Is it possible to overcome this by using only annotations without
> > changing the code?
> > The package specification and body, as well as the error messages are
> > shown below:
>
> > -- File P2.ads
> > --# inherit P1;
> > package P2
> > is
> >    procedure Proc;
> >    --# global in out P1.Val;
> >    --# derives P1.Val from P1.Val;
> >    --# post (P1.Val <= C1 -> P1.Val = 0) and  -- error appears here
> >    --#      (P1.Val >= C2 -> P1.Val = 1);     -- error appears here
>
> > end P2;
>
> > -- File P2.adb
> > with P1;
> > package body P2 is
>
> >    C1: constant P1.Type := 10;
> >    C2: constant P1.Type := 20;
>
> >    procedure Proc
> >    is
> >       V1: P1.Type;
> >    begin
> >       V1 := P1.Val;
> >       if V1 <= C1 then
> >          P1.Val := 0;
> >       elsif V1 >= C2 then
> >          P1.Val := 1;
> >       end if;
> >    end Proc;
>
> > end P2;
>
> > OUTPUT
> > 13:30   Semantic Error   1 - The identifier C1 is either undeclared or
> > not visible at this point.
> > 14:30   Semantic Error   1 - The identifier C2 is either undeclared or
> > not visible at this point.
>
> It always helps if complete (examinable) code is supplied - in this
> case there seems to be a type declared in the package P1 called "Type"
> - which can't be valid.
>
> The constants C1 and C2 are not visible in P2 specification as they
> aren't declared until the body.
>
> If you don't want to move these declarations to the specification then
> you can use parameterless proof functions to reference their values:
>
> --# function C1_Value return P1.Type;
> --# function C2_Value return P1.Type;
>
> In theory you can use these functions in the postcondition in the
> specification and provide a refined postcondition on the body of Proc
> that does reference C1 and C2 - then you just need two user rules to
> discharge the resulting refinement VC:
> p1_user(1): c1_value may_be_replaced by 10;
> p1_user(2): c2_value may_be_replaced by 20;
>
> BUT - there is an defect in the current (ie GPL 2010) version of SPARK
> where this may generate incorrect VCs for Proc.  This seems to occur
> when a pre- and/or post-condition is refined but there is no refined
> information flow (ie the derives annotation).  I don't know of any
> reliable workaround for this.
> (I understand that the SPARK team have fixed this defect, so if you
> are a supported customer you should be able to get an updated
> Examiner.)
>
> If you are using the GPL version, and can't use a refined
> postcondition, then just use the proof functions in the postcondition
> in the spec and the above two rules - plus any others that are needed
> - to discharge the resulting VCs.
>
> Cheers,
>
> Phil- Απόκρυψη κειμένου σε παράθεση -
>
> - Εμφάνιση κειμένου σε παράθεση -

Thank you very much for your response.