Re: My bug or else regarding Visibility Rules

[Simon Wright <simon@pushface.org>]

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