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,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.237.33.183 with SMTP id l52mr25894730qtc.2.1509237085688;
        Sat, 28 Oct 2017 17:31:25 -0700 (PDT)
X-Received: by 10.157.14.201 with SMTP id 67mr517510otj.4.1509237085653; Sat,
 28 Oct 2017 17:31:25 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!border1.nntp.ams1.giganews.com!nntp.giganews.com!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!k31no4466684qta.1!news-out.google.com!v14ni2705qtc.0!nntp.google.com!k31no4466682qta.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sat, 28 Oct 2017 17:31:25 -0700 (PDT)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=2601:18f:900:f900:6600:6aff:fe37:6bdc;
 posting-account=3pYsyQoAAACcI-ym7XtMOI2PDU8gRZS5
NNTP-Posting-Host: 2601:18f:900:f900:6600:6aff:fe37:6bdc
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <81f4fbf9-fef3-4592-a95e-64889e564df4@googlegroups.com>
Subject: What am I doing wrong with contracts?  Why are they succeeding when
 they should be failing?
From: Andrew Shvets <andrew.shvets@gmail.com>
Injection-Date: Sun, 29 Oct 2017 00:31:25 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 2246
X-Received-Body-CRC: 3069163692
Xref: news.eternal-september.org comp.lang.ada:48620
Date: 2017-10-28T17:31:25-07:00
List-Id: <comp.lang.ada>

This is the piece of code that I whipped up (Int_Array is an array of integ=
ers):

procedure Multiply_By_Two(Arr : in out Int_Array)
  with Pre  =3D> (for all Item in Arr'Range =3D>
                  Arr(Item) /=3D 6),
       Post =3D> (for all Item in Arr'Range =3D>
                  Arr(Item) =3D Arr'Old(Item) * 2);


And the implementation in the package:

procedure Multiply_By_Two(
  Arr : in out Int_Array) is

begin
  for iter in Arr'Range loop
    Arr(iter) :=3D Arr(iter) * 2;
  end loop;
end Multiply_By_Two;


I simply pass in the array into Multiply_By_Two and then print out the arra=
y as needed.  This is what gets me.  The array has elements going from 6 to=
 45.  The "Pre" aspect that I created should raise an exception that the pa=
ssed in element does not meet the conditions for the function to execute su=
ccessfully.  However, that is not the case.  Why?  I was under the impressi=
on that this contract will begin raising exceptions when the Pre aspect eva=
luates to the condition of False.

Am I missing something?  A compiler flag?

Thank you in advance.