SPARK: Problem with using constants in a post annotation

SPARK: Problem with using constants in a post annotation

[George]

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 Control;
   --# global in out P1.Val;
   --# derives P1.Val from P1.Val;
   --# post (P1.Val <= [COLOR="Red"][B]C1[/B][/COLOR] -> P1.Val = 0)
and
   --#      (P1.Val >= [COLOR="Red"][B]C2[/B][/COLOR] -> P1.Val = 1);

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.

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

[George]

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.

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

[Phil Thornley]

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

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

[George]

I can modify the question of the problem:

If we have to use a global variable in a post annotation, we must use
first own and global annotations, so that the variable is visible to
the post annotation. However, this cannot be done with constants. So,
how can I use a constant in a post annotation (the constant is
declared in the same package that is annotated)?

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

[George]

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.

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

[Mark Lorenzen]

On 13 Jan., 12:15, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
>
> 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.)
>

It would be really nice if AdaCore would issue an update to the GPL
version as well. I understand they can't update the GPL version every
time they issue a new wavefront release of a supported product, but
this bug has no workaround and it gives a bad impression of SPARK.

- Mark L

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

[Phil Thornley]

On Jan 17, 11:08 am, Mark Lorenzen <mark.loren...@gmail.com> wrote:
[...]
> It would be really nice if AdaCore would issue an update to the GPL
> version as well. I understand they can't update the GPL version every
> time they issue a new wavefront release of a supported product, but
> this bug has no workaround and it gives a bad impression of SPARK.

Looks like this wish has been answered.  Adacore have just announced a
new version of SPARK GPL.

The main change is the preview of the SPARKBridge technology which
allows SMT solvers to be used along with the Simplifier.  The release
note says that this error in VC generation has been fixed.

Cheers,

Phil

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

[Mark Lorenzen]

On 17 Jan., 16:17, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> Looks like this wish has been answered.  Adacore have just announced a
> new version of SPARK GPL.
>
> The main change is the preview of the SPARKBridge technology which
> allows SMT solvers to be used along with the Simplifier.  The release
> note says that this error in VC generation has been fixed.
>
> Cheers,
>
> Phil

Fantastic! I'm also very happy about J812-010 "Improve reasoning with
unit range quantified conclusions". Any improvement that helps the
user write (and discharge) loop invariants is very welcome.

- Mark L