From: Shark8 <onewingedshark@gmail.com>
Subject: Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
Date: Sun, 29 Oct 2017 17:16:42 -0700 (PDT)
Date: 2017-10-29T17:16:42-07:00 [thread overview]
Message-ID: <ef7f0ad9-a544-4823-aa81-64b4ba962450@googlegroups.com> (raw)
In-Reply-To: <81f4fbf9-fef3-4592-a95e-64889e564df4@googlegroups.com>
> procedure Multiply_By_Two(Arr : in out Int_Array)
> with Pre => (for all Item in Arr'Range =>
> Arr(Item) /= 6),
> Post => (for all Item in Arr'Range =>
> Arr(Item) = Arr'Old(Item) * 2);
>
>
> I simply pass in the array into Multiply_By_Two and then print out the array as needed. This is what gets me. The array has elements going from 6 to 45.
Your precondition is wrong then, all it's checking is that the [elements of the] inputs aren't 6, leaving things like 2 or 3 (or -17) as valid. I would recommend something like "with Pre => (for all Item in Arr'Range => Arr(Item) in 6..45)".
next prev parent reply other threads:[~2017-10-30 0:16 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-29 0:31 What am I doing wrong with contracts? Why are they succeeding when they should be failing? Andrew Shvets
2017-10-29 0:34 ` Andrew Shvets
2017-10-29 2:42 ` Andrew Shvets
2017-10-29 7:20 ` joakimds
2017-10-29 13:42 ` Andrew Shvets
2017-10-29 19:17 ` Anh Vo
2017-10-29 19:41 ` Andrew Shvets
2017-10-30 0:16 ` Shark8 [this message]
2017-10-30 1:37 ` Andrew Shvets
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox