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

[Phil Thornley <phil.jpthornley@gmail.com>]

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