My bug or else regarding Visibility Rules

My bug or else regarding Visibility Rules

[Anh Vo]

For the codes below GNAT complains that In_Index, Buffer, and Out_Index are undefined. However, if I comment out private key word, GNAT is happy. Did I violate Ada syntax rules? Thanks.


generic
   type Element is private;
   Length : Positive := 1;

package Circular_Queue is

   -- Indicates incorrect usage
   Queue_Error : Exception;

   -- Places an item in the queue.
   procedure Put (Item : Element)
     with pre => not Queue_Full,
          Post => (In_Index = In_Index'Old mod Length + 1) and
                  (Buffer(In_Index'Old) = Item) and 
                  (for all I in 1 .. Queue_Length'Old =>
                                Buffer(I) = Buffer'Old (I)) and 
                  (not Queue_Empty);
  
   -- Takes an item from the queue.
   function Get return Element
      with pre => not Queue_Empty,
           Post => (Out_Index = Out_Index'Old mod Length + 1) and
                   (Buffer(Out_Index'Old) = Get'Result) and 
                   (for all I in 1 .. Queue_Length =>
                                 Buffer(I) = Buffer'Old (I)) and 
                   (not Queue_Full);

   -- Returns the depth of the queue
   function Queue_Length return Natural;

   -- Indicates if the queue is full or not
   function Queue_Full return Boolean;

   -- Indicates if the queue is empty or not
   function Queue_Empty return Boolean;

private
   subtype Index is Positive range 1 .. Length;
   type Element_Array is array (Index) of Element;

   Buffer : Element_Array;
   In_Index : Index := 1;
   Out_Index : Index := 1;
   Count: Natural range 0 .. Length := 0;
end Circular_Queue;

Re: My bug or else regarding Visibility Rules

[Adam Beneschan]

On Thursday, March 28, 2013 12:54:26 PM UTC-7, Anh Vo wrote:
> For the codes below GNAT complains that In_Index, Buffer, and Out_Index are undefined. However, if I comment out private key word, GNAT is happy. Did I violate Ada syntax rules? Thanks.

13.1.1(11): The usage names in an aspect_definition [ are not resolved at the point of the associated declaration, but rather] are resolved at the end of the immediately enclosing declaration list.

In your example, the "immediately enclosing declaration list" ends at the keyword PRIVATE when that keyword is present; but if you take it out, the declaration list ends at "end Circular_Queue;".

                        -- Adam

Re: My bug or else regarding Visibility Rules

[Randy Brukardt]

"Adam Beneschan" <adam@irvine.com> wrote in message 
news:25ee066d-3270-4efd-829f-ed40b04c0655@googlegroups.com...
> On Thursday, March 28, 2013 12:54:26 PM UTC-7, Anh Vo wrote:
>> For the codes below GNAT complains that In_Index, Buffer, and Out_Index 
>> are undefined.
> However, if I comment out private key word, GNAT is happy. Did I violate 
> Ada syntax rules? Thanks.
>
> 13.1.1(11): The usage names in an aspect_definition [ are not resolved at 
> the point of the
>associated declaration, but rather] are resolved at the end of the 
>immediately enclosing declaration list.
>
> In your example, the "immediately enclosing declaration list" ends at the 
> keyword PRIVATE
> when that keyword is present; but if you take it out, the declaration list 
> ends at "end Circular_Queue;".

Which is the long way to say that the expression of a public aspect has to 
be made up only of public functions and objects. Otherwise, how would a 
caller be able to figure out the meaning of a precondition that they are 
required to meet? Clients can never be required to look in a private part.

This, BTW, is one of the reasons we added expression functions to Ada 2012. 
For a lot of these cases, you might as well let the compiler know what the 
actual object is, because then it probably can generate better code and 
possibly remove part or all of some of these checks. Thus using a function 
completed with an expression function in the private part essentially lets 
the compiler "peek" into private part. (Peeking into bodies is much harder, 
especially as bodies can be changed without changing the specification.)

                                             Randy.

Re: My bug or else regarding Visibility Rules

[Anh Vo]

On Thursday, March 28, 2013 1:58:33 PM UTC-7, Adam Beneschan wrote:
>> On Thursday, March 28, 2013 12:54:26 PM UTC-7, Anh Vo wrote: 
>> For the codes below GNAT complains that In_Index, Buffer, and Out_Index 
>> are undefined. However, if I comment out private key word, GNAT is happy.
>> Did I violate Ada syntax rules? Thanks. 

> 13.1.1(11): The usage names in an aspect_definition [ are not resolved at the > point of the associated declaration, but rather] are resolved at the end 
> of the immediately enclosing declaration list. 
> In your example, the "immediately enclosing declaration list" ends at the 
> keyword PRIVATE when that keyword is present; but if you take it out, the
> declaration list ends at "end Circular_Queue;". -- Adam
 
I understand it now. Thank you Adam for your help. By the way, I have decided to move these data into the body event though I will lose parts of Postcondition checking.

AVo 

Re: My bug or else regarding Visibility Rules

[Anh Vo]

On Thursday, March 28, 2013 3:03:13 PM UTC-7, Randy Brukardt wrote:
> "Adam Beneschan" <adam@irvine.com> wrote in message  
> news:25ee066d-3270-4efd-829f-ed40b04c0655@googlegroups.com... 
> > On Thursday, March 28, 2013 12:54:26 PM UTC-7, Anh Vo wrote:
> >> For the codes below GNAT complains that In_Index, Buffer, and Out_Index 
> >> are undefined. 
> > However, if I comment out private key word, GNAT is happy. Did I violate 
> > Ada syntax rules? Thanks. 
> > 
> > 13.1.1(11): The usage names in an aspect_definition [ are not resolved at  
> > the point of the 
> >associated declaration, but rather] are resolved at the end of the  
> >immediately enclosing declaration list. 
> > 
> > In your example, the "immediately enclosing declaration list" ends at the  
> > keyword PRIVATE 
> > when that keyword is present; but if you take it out, the declaration list  
> > ends at "end Circular_Queue;".  
> 
> Which is the long way to say that the expression of a public aspect has to  
> be made up only of public functions and objects. Otherwise, how would a  
> caller be able to figure out the meaning of a precondition that they are  
> required to meet? Clients can never be required to look in a private part.

Actually, this part only involves post-conditions (implementer), not preconditions (clients). 
 
A. Vo

Re: My bug or else regarding Visibility Rules

[Randy Brukardt]

"Anh Vo" <anhvofrcaus@gmail.com> wrote in message 
news:89292c53-1d4e-48a7-b2ae-a10983ef4168@googlegroups.com...
> On Thursday, March 28, 2013 3:03:13 PM UTC-7, Randy Brukardt wrote:
>> "Adam Beneschan" <adam@irvine.com> wrote in message
>> news:25ee066d-3270-4efd-829f-ed40b04c0655@googlegroups.com...
>> > On Thursday, March 28, 2013 12:54:26 PM UTC-7, Anh Vo wrote:
>> >> For the codes below GNAT complains that In_Index, Buffer, and 
>> >> Out_Index
>> >> are undefined.
>> > However, if I comment out private key word, GNAT is happy. Did I 
>> > violate
>> > Ada syntax rules? Thanks.
>> >
>> > 13.1.1(11): The usage names in an aspect_definition [ are not resolved 
>> > at
>> > the point of the
>> >associated declaration, but rather] are resolved at the end of the
>> >immediately enclosing declaration list.
>> >
>> > In your example, the "immediately enclosing declaration list" ends at 
>> > the
>> > keyword PRIVATE
>> > when that keyword is present; but if you take it out, the declaration 
>> > list
>> > ends at "end Circular_Queue;".
>>
>> Which is the long way to say that the expression of a public aspect has 
>> to
>> be made up only of public functions and objects. Otherwise, how would a
>> caller be able to figure out the meaning of a precondition that they are
>> required to meet? Clients can never be required to look in a private 
>> part.
>
> Actually, this part only involves post-conditions (implementer), not 
> preconditions (clients).

Clients need to know about postconditions as well, so that they know what 
properties are guaranteed after a call. Typically, that will show that some 
or all of a following precondition is going to be satisfied. Remember, both 
of these matter to both sides of a call:

A precondition is a requirement on a caller and a promise to an 
implementation; a postcondition is a promise to a caller and a requirement 
on an implementation.

                                      Randy.

Re: My bug or else regarding Visibility Rules

[Anh Vo]

On Monday, April 1, 2013 5:56:19 PM UTC-7, Randy Brukardt wrote:
> "Anh Vo" <anhvofrcaus@gmail.com> wrote in message news:89292c53-1d4e-48a7-b2ae-a10983ef4168@googlegroups.com... > On Thursday, March 28, 2013 3:03:13 PM UTC-7, Randy Brukardt wrote: >> "Adam Beneschan" <adam@irvine.com> wrote in >>> the >> > keyword PRIVATE >> > when that keyword is present; but if you take it out, the declaration >> > list >> > ends at "end Circular_Queue;". >> 
>>> Which is the long way to say that the expression of a public aspect has
>>> be made up only of public functions and objects. Otherwise, how would a 
>>> caller be able to figure out the meaning of a precondition that they are 
>>> required to meet? Clients can never be required to look in a private 
>>> part. 

>> Actually, this part only involves post-conditions (implementer), not 
>> preconditions (clients). 

>Clients need to know about postconditions as well, so that they know what >properties are guaranteed after a call. Typically, that will show that 
>some or all of a following precondition is going to be satisfied. Remember, >both of these matter to both sides of a call: A precondition is a requirement >on a caller and a promise to an implementation; a postcondition is a promise >to a caller and a requirement on an implementation. Randy.

I try to put as much as post-conditions that the language allows. On the other hand, I do not want to expose any thing that the clients can modify. In addition, taking away post-conditions involving Buffer, In_Index, and Out_Index objects by moving them into the body does degrade much implementation promise in this case.

A. Vo   

Re: My bug or else regarding Visibility Rules

[Simon Wright]

Anh Vo <anhvofrcaus@gmail.com> writes:

> I try to put as much as post-conditions that the language allows. On
> the other hand, I do not want to expose any thing that the clients can
> modify. In addition, taking away post-conditions involving Buffer,
> In_Index, and Out_Index objects by moving them into the body does
> degrade much implementation promise in this case.

This is (partly) why we now have expression functions; specify the
function in the public part, use it in a pre/postcondition, complete it
with an expression function in the private part when Buffer etc. are
visible.

Re: My bug or else regarding Visibility Rules

[Anh Vo]

On Tuesday, April 2, 2013 1:26:12 AM UTC-7, Simon Wright wrote:
Other recipients: 
Anh Vo <anhvo...@gmail.com> writes: 
> This is (partly) why we now have expression functions; specify the 
> function in the public part, use it in a pre/postcondition, complete it 
> with an expression function in the private part when Buffer etc. are 
> visible. 

It is dangerous make internal data visible in this case. after careful consideration, I decided to take away part of the post-conditions rather than exposing them. Following the philosophy of Ada, I would not leave any possibilities for the clients to accidently mess it up (not allowing clients to shoot themselve in the foot)

Re: My bug or else regarding Visibility Rules

[Simon Wright]

Anh Vo <anhvofrcaus@gmail.com> writes:

> On Tuesday, April 2, 2013 1:26:12 AM UTC-7, Simon Wright wrote:
> Other recipients: 
> Anh Vo <anhvo...@gmail.com> writes: 
>> This is (partly) why we now have expression functions; specify the 
>> function in the public part, use it in a pre/postcondition, complete it 
>> with an expression function in the private part when Buffer etc. are 
>> visible. 
>
> It is dangerous make internal data visible in this case. after careful
> consideration, I decided to take away part of the post-conditions
> rather than exposing them. Following the philosophy of Ada, I would
> not leave any possibilities for the clients to accidently mess it up
> (not allowing clients to shoot themselve in the foot)

I think that part of your difficulty is that your Queue is implemented
using (effectively) global objects (Buffer, In_Index etc). If you made
Queue a data type

   type Queue is private;
   ...
private
   ...
   type Queue is record
      Buffer : Element_Array;
      In_Index : Index := 1;
      Out_Index : Index := 1;
      Count: Natural range 0 .. Length := 0;
   end record;

then you could say something like

   procedure Put (Q : in out Queue; Item : Element)
     with Pre => not Queue_Full (Q'Old),
          Post => Item_Added (Q'Old, Q, Item);

with public

   function Item_Added (Old, Current : Queue; Item : Element) return Boolean;

and private

   function Item_Added
     (Old, Current : Queue; Item : Element) return Boolean is
      ((Current.In_Index = (Old.In_Index + 1) mod Length) and
         (Current.Buffer (Old.In_Index) = Item) and
--         (for all I in 1 .. Queue_Length'Old =>
--            Buffer(I) = Buffer'Old (I)) and
         (not Queue_Empty (Current)));

Notes:

I commented out the comparison, because this is a *circular* buffer, so
the first valid element isn't at Buffer(1).

I think it will all work better if you say
   subtype Index is Natural range 0 .. Length - 1;
so that mod works as you require.

You need to add 1 to the current index and then do mod length!   

Re: My bug or else regarding Visibility Rules

[Randy Brukardt]

"Anh Vo" <anhvofrcaus@gmail.com> wrote in message 
news:d09afc35-2ca5-4b45-9734-7263e6d353c4@googlegroups.com...
On Monday, April 1, 2013 5:56:19 PM UTC-7, Randy Brukardt wrote:
...
>>Clients need to know about postconditions as well, so that they know what
>>properties are guaranteed after a call. Typically, that will show that
>>some or all of a following precondition is going to be satisfied. 
>>Remember,
>>both of these matter to both sides of a call: A precondition is a 
>>requirement
>>on a caller and a promise to an implementation; a postcondition is a 
>>promise
>>to a caller and a requirement on an implementation.

>I try to put as much as post-conditions that the language allows. On the 
>other hand,
>I do not want to expose any thing that the clients can modify. In addition, 
>taking away
>post-conditions involving Buffer, In_Index, and Out_Index objects by moving 
>them
>into the body does degrade much implementation promise in this case.

The only things that should be in Post aspects are those that the client 
might care about.

We've talked a bit about "body postconditions" that wouldn't be visible to 
the client. That's what you want here, but Ada doesn't have that yet. Talk 
to your vendor and convince them to support Body_Post or something like that 
(implementation-defined aspects are allowed, just like 
implementation-defined attributes are allowed).

                                          Randy.

Re: My bug or else regarding Visibility Rules

[Anh Vo]

On Tuesday, April 2, 2013 1:16:34 PM UTC-7, Simon Wright wrote:
> Anh Vo <anhvofrcaus@gmail.com> writes: > On Tuesday, April 2, 2013 1:26:12 AM UTC-7, Simon Wright wrote: > Other recipients: > Anh Vo <anhvo...@gmail.com> writes: 

>> It is dangerous make internal data visible in this case. after careful 
>> consideration, I decided to take away part of the post-conditions 
>> rather than exposing them. Following the philosophy of Ada, I would 
>> not leave any possibilities for the clients to accidently mess it up 
>> (not allowing clients to shoot themselve in the foot) 

> I think that part of your difficulty is that your Queue is implemented 
> using(effectively) global objects (Buffer, In_Index etc). 

Actually, it is my intention to design this way. I believe it is called singleton form. I could have designed Queue type as well, as you suggested. 

> then you could say something like 
>
>   procedure Put (Q : in out Queue; Item : Element) 
>     with Pre => not Queue_Full (Q'Old), 
>          Post => Item_Added (Q'Old, Q, Item); 

I believe that attribute 'Old is allowed in post-conditions only. 

> with public 
>
>   function Item_Added (Old, Current : Queue; Item : Element) return Boolean; 
>
>and private 
>
>   function Item_Added 
>     (Old, Current : Queue; Item : Element) return Boolean is 
>      ((Current.In_Index = (Old.In_Index + 1) mod Length) and 
>         (Current.Buffer (Old.In_Index) = Item) and 
> --         (for all I in 1 .. Queue_Length'Old => 
> --            Buffer(I) = Buffer'Old (I)) and 
>         (not Queue_Empty (Current))); 

This way does not look simpler. I rather go with simple way even I decide to use Queue type instead of Singleton Queue.

> I commented out the comparison, because this is a *circular* buffer, so 
> the first valid element isn't at Buffer(1).

I do not understand this. Why isn't Buffer(1) valid if my index starts at 1? 

> I think it will all work better if you say 
>   subtype Index is Natural range 0 .. Length - 1; 
> so that mod works as you require. 
>
> You need to add 1 to the current index and then do mod length! 

This is another array index option.

A. Vo

Re: My bug or else regarding Visibility Rules

[Simon Wright]

Anh Vo <anhvofrcaus@gmail.com> writes:

> On Tuesday, April 2, 2013 1:16:34 PM UTC-7, Simon Wright wrote:

>>   procedure Put (Q : in out Queue; Item : Element) 
>>     with Pre => not Queue_Full (Q'Old), 
>>          Post => Item_Added (Q'Old, Q, Item); 
>
> I believe that attribute 'Old is allowed in post-conditions only. 

This is a bug in GNAT, fixed in GCC 4.8.0 (I had tested with GNAT GPL
2012, which allows it).

>> with public 
>>
>>   function Item_Added (Old, Current : Queue; Item : Element) return Boolean; 
>>
>>and private 
>>
>>   function Item_Added 
>>     (Old, Current : Queue; Item : Element) return Boolean is 
>>      ((Current.In_Index = (Old.In_Index + 1) mod Length) and 
>>         (Current.Buffer (Old.In_Index) = Item) and 
>> --         (for all I in 1 .. Queue_Length'Old => 
>> --            Buffer(I) = Buffer'Old (I)) and 
>>         (not Queue_Empty (Current))); 
>
> This way does not look simpler. I rather go with simple way even I
> decide to use Queue type instead of Singleton Queue.

Not simpler, just the only way I can see to retain privacy and
contracts.

>> I commented out the comparison, because this is a *circular* buffer, so 
>> the first valid element isn't at Buffer(1).
>
> I do not understand this. Why isn't Buffer(1) valid if my index starts at 1? 

Because after the index has wrapped round Buffer'Old(1) will not be the
same as Buffer(1).

>> I think it will all work better if you say 
>>   subtype Index is Natural range 0 .. Length - 1; 
>> so that mod works as you require. 
>>
>> You need to add 1 to the current index and then do mod length! 
>
> This is another array index option.

No. You wrote
   (Index mod Length) + 1
but it should be
   (Index + 1) mod Length

Re: My bug or else regarding Visibility Rules

[Anh Vo]

On Thursday, April 4, 2013 1:19:54 AM UTC-7, Simon Wright wrote:
> Anh Vo <anhvofrcaus@gmail.com> writes: > On Tuesday, April 2, 2013 1:16:34 PM UTC-7, Simon Wright wrote:

>> I believe that attribute 'Old is allowed in post-conditions only. 

> This is a bug in GNAT, fixed in GCC 4.8.0 (I had tested with GNAT GPL 
> 2012, which allows it). 

It is good to know.

>> I do not understand this. Why isn't Buffer(1) valid if my index starts at 1? 

> Because after the index has wrapped round Buffer'Old(1) will not be the 
> same as Buffer(1). 

In this case the loop will drop out because loop lower end is greater than loop upper end.

>> This is another array index option. 

> No. You wrote 
>   (Index mod Length) + 1 
> but it should be 
>   (Index + 1) mod Length 

(In_Index + 1) mod length will raise Constraint_Error when the Queue is just full. In fact, (10 + 1) > 10 when the queue has the lenght of 10.

Re: My bug or else regarding Visibility Rules

[Simon Wright]

Anh Vo <anhvofrcaus@gmail.com> writes:

> On Thursday, April 4, 2013 1:19:54 AM UTC-7, Simon Wright wrote:
>> Anh Vo <anhvofrcaus@gmail.com> writes: > On Tuesday, April 2, 2013
>> 1:16:34 PM UTC-7, Simon Wright wrote:

>>> I do not understand this. Why isn't Buffer(1) valid if my index
>>> starts at 1?
>
>> Because after the index has wrapped round Buffer'Old(1) will not be the 
>> same as Buffer(1). 
>
> In this case the loop will drop out because loop lower end is greater
> than loop upper end.

Consider a queue of max length 5 containing letters. 5 letters (a, b, c,
d, e) have been Put, and one (a) Got.

   I
   a b c d e
     O

After the next letter is inserted, you'd have

     I
   f b c d e
     O

Your check is

   (for all I in 1 .. Queue_Length'Old =>
                 Buffer(I) = Buffer'Old (I))

which is going to fail.

>> No. You wrote 
>>   (Index mod Length) + 1 
>> but it should be 
>>   (Index + 1) mod Length 
>
> (In_Index + 1) mod length will raise Constraint_Error when the Queue
> is just full. In fact, (10 + 1) > 10 when the queue has the lenght of
> 10.

OK, I've never seen this way of managing an index but I can see it
working. Still think that 0-based is easier.

That said, (In_Index + 1) won't raise CE, because Index is a subtype and
inherits the operations of Integer. CE on assignment, sure, but the 'mod
Length' would have been applied by then.