INTELLIGENT WORK FORUMS
FOR COMPUTER PROFESSIONALS

Log In

Come Join Us!

Are you a
Computer / IT professional?
Join Tek-Tips Forums!
  • Talk With Other Members
  • Be Notified Of Responses
    To Your Posts
  • Keyword Search
  • One-Click Access To Your
    Favorite Forums
  • Automated Signatures
    On Your Posts
  • Best Of All, It's Free!

*Tek-Tips's functionality depends on members receiving e-mail. By joining you are opting in to receive e-mail.

Posting Guidelines

Promoting, selling, recruiting, coursework and thesis posting is forbidden.

Jobs

SPARK: Problem with using constants in post annotation

SPARK: Problem with using constants in post annotation

SPARK: Problem with using constants in post annotation

(OP)
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? 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 <= C1 -> P1.Val = 0) and  -- 1st error
   --#      (P1.Val >= C2 -> P1.Val = 1);     -- 2nd error

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 post annotation

I don't know SPARK but at a guess C1 and C2 have to be declared as global.

RE: SPARK: Problem with using constants in post annotation

(OP)
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)?

Red Flag This Post

Please let us know here why this post is inappropriate. Reasons such as off-topic, duplicates, flames, illegal, vulgar, or students posting their homework.

Red Flag Submitted

Thank you for helping keep Tek-Tips Forums free from inappropriate posts.
The Tek-Tips staff will check this out and take appropriate action.

Reply To This Thread

Posting in the Tek-Tips forums is a member-only feature.

Click Here to join Tek-Tips and talk with other members!

Resources

Close Box

Join Tek-Tips® Today!

Join your peers on the Internet's largest technical computer professional community.
It's easy to join and it's free.

Here's Why Members Love Tek-Tips Forums:

Register now while it's still free!

Already a member? Close this window and log in.

Join Us             Close