Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?

[Andrew Shvets <andrew.shvets@gmail.com>]

On Sunday, October 29, 2017 at 8:16:43 PM UTC-4, Shark8 wrote:
> > 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)".

I did that on purpose.  I was trying to figure out why my logic wasn't working, so I used a blatantly wrong comparison (the array did have one 6 in it, so I should have seen an error.)