* What am I doing wrong with contracts? Why are they succeeding when they should be failing?
@ 2017-10-29 0:31 Andrew Shvets
2017-10-29 0:34 ` Andrew Shvets
2017-10-30 0:16 ` Shark8
0 siblings, 2 replies; 9+ messages in thread
From: Andrew Shvets @ 2017-10-29 0:31 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
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-30 0:16 ` Shark8
1 sibling, 1 reply; 9+ messages in thread
From: Andrew Shvets @ 2017-10-29 0:34 UTC (permalink / raw)
I think I'm misunderstanding how proofs/contracts work at some fundamental level. Hence my confusion.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
2017-10-29 0:34 ` Andrew Shvets
@ 2017-10-29 2:42 ` Andrew Shvets
2017-10-29 7:20 ` joakimds
0 siblings, 1 reply; 9+ messages in thread
From: Andrew Shvets @ 2017-10-29 2:42 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
2017-10-29 2:42 ` Andrew Shvets
@ 2017-10-29 7:20 ` joakimds
2017-10-29 13:42 ` Andrew Shvets
0 siblings, 1 reply; 9+ messages in thread
From: joakimds @ 2017-10-29 7:20 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
2017-10-29 7:20 ` joakimds
@ 2017-10-29 13:42 ` Andrew Shvets
2017-10-29 19:17 ` Anh Vo
0 siblings, 1 reply; 9+ messages in thread
From: Andrew Shvets @ 2017-10-29 13:42 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
2017-10-29 13:42 ` Andrew Shvets
@ 2017-10-29 19:17 ` Anh Vo
2017-10-29 19:41 ` Andrew Shvets
0 siblings, 1 reply; 9+ messages in thread
From: Anh Vo @ 2017-10-29 19:17 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
2017-10-29 19:17 ` Anh Vo
@ 2017-10-29 19:41 ` Andrew Shvets
0 siblings, 0 replies; 9+ messages in thread
From: Andrew Shvets @ 2017-10-29 19:41 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
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-30 0:16 ` Shark8
2017-10-30 1:37 ` Andrew Shvets
1 sibling, 1 reply; 9+ messages in thread
From: Shark8 @ 2017-10-30 0:16 UTC (permalink / raw)
> 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)".
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
2017-10-30 0:16 ` Shark8
@ 2017-10-30 1:37 ` Andrew Shvets
0 siblings, 0 replies; 9+ messages in thread
From: Andrew Shvets @ 2017-10-30 1:37 UTC (permalink / raw)
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.)
^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2017-10-30 1:37 UTC | newest]
Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
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
2017-10-30 1:37 ` Andrew Shvets
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox