Is there any difference between these two methods of implementing a precondition?:

-----------------------
void foo(int x)
in {
   // do some checking
}
body
{
   ...
}
-----------------------

and this:

-----------------------
void foo(int x)
{
  debug {
     // do some checking
  }
  ...
}
-----------------------

And if "some checking" is just an assert() or two is there any difference between the 'in' precondition version and just plain

-----------------------
void foo(int x)
{
  assert(something, "something's not right");
  ...
}
-----------------------


Just curious.  Typing 'in' and 'body' just doesn't come naturally to me.  But I've seen plenty of D code with an in{}body{} pair where the in{} only contains one assert(), so I was wondering if there was some advantage to the extra verbiage that I was missing out on.

--bb

Bill Baxter wrote:
> Is there any difference between these two methods of implementing a precondition?:
> 
> -----------------------
> void foo(int x)
> in {
>    // do some checking
> }
> body
> {
>    ...
> }
> -----------------------
> 
> and this:
> 
> -----------------------
> void foo(int x)
> {
>   debug {
>      // do some checking
>   }
>   ...
> }
> -----------------------

I think the primary difference is that debug sections are only compiled in if you throw the -debug switch, whereas contracts are *omitted* if you throw the -release switch.

> And if "some checking" is just an assert() or two is there any difference between the 'in' precondition version and just plain
> 
> -----------------------
> void foo(int x)
> {
>   assert(something, "something's not right");
>   ...
> }
> -----------------------

AFAIK, there isn't.  Well, unless your assert is "assert(false)" which never gets thrown out, unless it's in the 'in' contract and you throw -release.

> Just curious.  Typing 'in' and 'body' just doesn't come naturally to me.
>  But I've seen plenty of D code with an in{}body{} pair where the in{}
> only contains one assert(), so I was wondering if there was some
> advantage to the extra verbiage that I was missing out on.
> 
> --bb

Code documentation, perhaps?  I like it because it provides a nice separation between contract assertions and the actual implementation.

	-- Daniel

Daniel Keep wrote:
> 
> Bill Baxter wrote:
>> Is there any difference between these two methods of implementing a
>> precondition?:
>>
>> -----------------------
>> void foo(int x)
>> in {
>>    // do some checking
>> }
>> body
>> {
>>    ...
>> }
>> -----------------------
>>
>> and this:
>>
>> -----------------------
>> void foo(int x)
>> {
>>   debug {
>>      // do some checking
>>   }
>>   ...
>> }
>> -----------------------
> 
> I think the primary difference is that debug sections are only compiled
> in if you throw the -debug switch, whereas contracts are *omitted* if
> you throw the -release switch.
> 
>> And if "some checking" is just an assert() or two is there any
>> difference between the 'in' precondition version and just plain
>>
>> -----------------------
>> void foo(int x)
>> {
>>   assert(something, "something's not right");
>>   ...
>> }
>> -----------------------
> 
> AFAIK, there isn't.  Well, unless your assert is "assert(false)" which
> never gets thrown out, unless it's in the 'in' contract and you throw
> -release.
> 
>> Just curious.  Typing 'in' and 'body' just doesn't come naturally to me.
>>  But I've seen plenty of D code with an in{}body{} pair where the in{}
>> only contains one assert(), so I was wondering if there was some
>> advantage to the extra verbiage that I was missing out on.
>>
>> --bb
> 
> Code documentation, perhaps?  I like it because it provides a nice
> separation between contract assertions and the actual implementation.
> 
> 	-- Daniel

Thanks.  Your answers sum it up very nicely.

--bb

Two more differences I can think of:

Contracts are only left out when you compile without release, thus using 'in-out-body' can be a way to compile in contracts without debug code. Not saying anything for or against this, but it's a possibility.

Contracts are also inherited although iirc this behavior isn't implemented.