From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,75ce2ead897158b2
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.180.92.202 with SMTP id co10mr2364453wib.1.1365343216664;
        Sun, 07 Apr 2013 07:00:16 -0700 (PDT)
Path: 
 p18ni42886wiv.0!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.103.MISMATCH!feeder3.cambriumusenet.nl!feed.tweaknews.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!news.n-ix.net!news.hufnagl.info!fu-berlin.de!news.swapon.de!eternal-september.org!feeder.eternal-september.org!mx05.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: My bug or else regarding Visibility Rules
Date: Tue, 02 Apr 2013 21:16:34 +0100
Organization: A noiseless patient Spider
Message-ID: <lysj38hen1.fsf@pushface.org>
References: <0c77e832-e12b-446d-af24-78d77c358f1e@googlegroups.com>
	<25ee066d-3270-4efd-829f-ed40b04c0655@googlegroups.com>
	<kj2en4$9q1$1@munin.nbi.dk>
	<89292c53-1d4e-48a7-b2ae-a10983ef4168@googlegroups.com>
	<kjdabm$dck$1@munin.nbi.dk>
	<d09afc35-2ca5-4b45-9734-7263e6d353c4@googlegroups.com>
	<lywqslgwyj.fsf@pushface.org>
	<e703d782-2e4c-4fe9-bcae-218abcc170f1@googlegroups.com>
Mime-Version: 1.0
Injection-Info: mx05.eternal-september.org;
 posting-host="72a7bb6120f61bc7749e29c9c2e535af";
	logging-data="23322"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+0s5fRKmGjuAJNfIg4Sij+PzdFJKgspuc="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.2 (darwin)
Cancel-Lock: sha1:3ztVj5XjIpGs0PErOhlAnKXS2wQ=
	sha1:dMzDjztWiq+1aGbAVwwtdlGRJIk=
Content-Type: text/plain
Date: 2013-04-02T21:16:34+01:00
List-Id: <comp.lang.ada>

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!