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

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

[Andrew Shvets]

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

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);


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) := Arr(iter) * 2;
  end loop;
end Multiply_By_Two;


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.  The "Pre" aspect that I created should raise an exception that the passed in element does not meet the conditions for the function to execute successfully.  However, that is not the case.  Why?  I was under the impression that this contract will begin raising exceptions when the Pre aspect evaluates to the condition of False.

Am I missing something?  A compiler flag?

Thank you in advance.

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

[Andrew Shvets]

I think I'm misunderstanding how proofs/contracts work at some fundamental level.  Hence my confusion.

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

[Andrew Shvets]

On Saturday, October 28, 2017 at 8:34:12 PM UTC-4, Andrew Shvets wrote:
> I think I'm misunderstanding how proofs/contracts work at some fundamental level.  Hence my confusion.

I figured it out, I needed to have the following at the top of where the contract was written in order to have it be checked/enforced:

pragma Assertion_Policy(Check);

I'm reading more about this right now.

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

[joakimds]

Den söndag 29 oktober 2017 kl. 03:42:07 UTC+1 skrev Andrew Shvets:
> On Saturday, October 28, 2017 at 8:34:12 PM UTC-4, Andrew Shvets wrote:
> > I think I'm misunderstanding how proofs/contracts work at some fundamental level.  Hence my confusion.
> 
> I figured it out, I needed to have the following at the top of where the contract was written in order to have it be checked/enforced:
> 
> pragma Assertion_Policy(Check);
> 
> I'm reading more about this right now.

To get run-time checks for the contracts you need to use the gcc Enable Assertions flag "-gnata" during compilation.

Best regards,
Joakim

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

[Andrew Shvets]

On Sunday, October 29, 2017 at 3:20:15 AM UTC-4, joak...@kth.se wrote:
> Den söndag 29 oktober 2017 kl. 03:42:07 UTC+1 skrev Andrew Shvets:
> > On Saturday, October 28, 2017 at 8:34:12 PM UTC-4, Andrew Shvets wrote:
> > > I think I'm misunderstanding how proofs/contracts work at some fundamental level.  Hence my confusion.
> > 
> > I figured it out, I needed to have the following at the top of where the contract was written in order to have it be checked/enforced:
> > 
> > pragma Assertion_Policy(Check);
> > 
> > I'm reading more about this right now.
> 
> To get run-time checks for the contracts you need to use the gcc Enable Assertions flag "-gnata" during compilation.
> 
> Best regards,
> Joakim

I just tried this.  It works.  Thanks for the tip.

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

[Anh Vo]

On Sunday, October 29, 2017 at 6:42:09 AM UTC-7, Andrew Shvets wrote:
> On Sunday, October 29, 2017 at 3:20:15 AM UTC-4, joak...@kth.se wrote:
> > Den söndag 29 oktober 2017 kl. 03:42:07 UTC+1 skrev Andrew Shvets:
> > > On Saturday, October 28, 2017 at 8:34:12 PM UTC-4, Andrew Shvets wrote:
> > > > I think I'm misunderstanding how proofs/contracts work at some fundamental level.  Hence my confusion.
> > > 
> > > I figured it out, I needed to have the following at the top of where the contract was written in order to have it be checked/enforced:
> > > 
> > > pragma Assertion_Policy(Check);
> > > 
> > > I'm reading more about this right now.
> > 
> > To get run-time checks for the contracts you need to use the gcc Enable Assertions flag "-gnata" during compilation.
> > 
> > Best regards,
> > Joakim
> 
> I just tried this.  It works.  Thanks for the tip.

I would prefer using pragma Assertion_Policy(Check) since it is 100% portable.

Anh Vo

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

[Andrew Shvets]

On Sunday, October 29, 2017 at 3:17:15 PM UTC-4, Anh Vo wrote:
> On Sunday, October 29, 2017 at 6:42:09 AM UTC-7, Andrew Shvets wrote:
> > On Sunday, October 29, 2017 at 3:20:15 AM UTC-4, joak...@kth.se wrote:
> > > Den söndag 29 oktober 2017 kl. 03:42:07 UTC+1 skrev Andrew Shvets:
> > > > On Saturday, October 28, 2017 at 8:34:12 PM UTC-4, Andrew Shvets wrote:
> > > > > I think I'm misunderstanding how proofs/contracts work at some fundamental level.  Hence my confusion.
> > > > 
> > > > I figured it out, I needed to have the following at the top of where the contract was written in order to have it be checked/enforced:
> > > > 
> > > > pragma Assertion_Policy(Check);
> > > > 
> > > > I'm reading more about this right now.
> > > 
> > > To get run-time checks for the contracts you need to use the gcc Enable Assertions flag "-gnata" during compilation.
> > > 
> > > Best regards,
> > > Joakim
> > 
> > I just tried this.  It works.  Thanks for the tip.
> 
> I would prefer using pragma Assertion_Policy(Check) since it is 100% portable.
> 
> Anh Vo

I agree.  That I'd forget the compiler flag from time to time and think my code was working when it wasn't.

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

[Shark8]

> 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)".

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

[Andrew Shvets]

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.)