Hi

In the manual http://www.digitalmars.com/d/dbc.html I read  :
" The pre contracts specify the preconditions before a statement is
executed. The most typical use of this would be in validating the parameters
to a function. The post contracts validate the result of the statement. The
most typical use of this would be in validating the return value of a
function and of any side effects it has. "
Makes sense to me. What I ask myself is if it's useful elsewhere and
especially is it possible in D? I tried it with a little example.

void main()
{
   bool assign = true;
   int x;
   in{
      assert(assign);
   }
   body{
      x = 1;
   }
}


It wont compile ("found in instead of statement"). I know it's not exactly a useful example but I just wanted to check if it was possible. I thought it would be because nowhere es said it's not possible. Did I just made a programming error or is it really not possible?

Greetings
Jan

You just got the syntax of the contracts slightly wrong.  This is the correct version:

bool fooFunc(Foo* f)
    in
    {
        assert(f !is null);
    }
    out (result)
    {
        assert(f.fooWasDone());
        assert(result == true);
    }
    body
    {
        bool fooVal;
        fooVal = f.doFoo();
        return fooVal;
    }

Note that the in, out, and body are not wrapped in curly braces and that the in and out contracts can't access variables from the body contract (because they are in different scopes), though the in and out contracts can access the arguments and the out contract can also access the return value (as an optional parameter passed to it).  Finally, keep in mind that the in and out contracts (like asserts) aren't included when the compiler is set to release mode so don't put critical error checking in them (they're intended to be used to help verify program correctness while you're developing the program).

"Tyler Knott" <tywebmail@mailcity.com> schreef in bericht news:f2ogbj$2kp6$1@digitalmars.com...
> You just got the syntax of the contracts slightly wrong.  This is the correct version:
>
> bool fooFunc(Foo* f)
>     in
>     {
>         assert(f !is null);
>     }
>     out (result)
>     {
>         assert(f.fooWasDone());
>         assert(result == true);
>     }
>     body
>     {
>         bool fooVal;
>         fooVal = f.doFoo();
>         return fooVal;
>     }
>
> Note that the in, out, and body are not wrapped in curly braces and that the in and out contracts can't access variables from the body contract (because they are in different scopes), though the in and out contracts can access the arguments and the out contract can also access the return value (as an optional parameter passed to it).  Finally, keep in mind that the in and out contracts (like asserts) aren't included when the compiler is set to release mode so don't put critical error checking in them (they're intended to be used to help verify program correctness while you're developing the program).

Actually I know all this, and I've been using it this way. Maybe the example I gave was a bit misleading but what I actualy want to know is if it's possible to use these pre- and postconditions somewhere else then with a function body. Because in the manual they state that with a funtion is "the most typical use", so I'm asking myself what the other uses could be.

Jan

Jan Hanselaer wrote:

> 
> "Tyler Knott" <tywebmail@mailcity.com> schreef in bericht news:f2ogbj$2kp6$1@digitalmars.com...
>> You just got the syntax of the contracts slightly wrong.  This is the correct version:
>>
>> bool fooFunc(Foo* f)
>>     in
>>     {
>>         assert(f !is null);
>>     }
>>     out (result)
>>     {
>>         assert(f.fooWasDone());
>>         assert(result == true);
>>     }
>>     body
>>     {
>>         bool fooVal;
>>         fooVal = f.doFoo();
>>         return fooVal;
>>     }
>>
>> Note that the in, out, and body are not wrapped in curly braces and that the in and out contracts can't access variables from the body contract (because they are in different scopes), though the in and out contracts can access the arguments and the out contract can also access the return value (as an optional parameter passed to it).  Finally, keep in mind that the in and out contracts (like asserts) aren't included when the compiler is set to release mode so don't put critical error checking in them (they're intended to be used to help verify program correctness while you're developing the program).
> 
> Actually I know all this, and I've been using it this way. Maybe the example I gave was a bit misleading but what I actualy want to know is if it's possible to use these pre- and postconditions somewhere else then with a function body. Because in the manual they state that with a funtion is "the most typical use", so I'm asking myself what the other uses could be.

Of course there could be other places too. One particularly interesting and useful feature would be support for contracts in interfaces. From the language user's point of view contracts aren't very polished or consistent at the moment. Hopefully they will be one of the important features on Walter's todo list right after the constness and ast macro stuff.

> 
> Jan

"Jari-Matti Mäkelä" <jmjmak@utu.fi.invalid> schreef in bericht news:f2p10j$fkf$1@digitalmars.com...
> Jan Hanselaer wrote:
>
>>
>> "Tyler Knott" <tywebmail@mailcity.com> schreef in bericht news:f2ogbj$2kp6$1@digitalmars.com...
>>> You just got the syntax of the contracts slightly wrong.  This is the correct version:
>>>
>>> bool fooFunc(Foo* f)
>>>     in
>>>     {
>>>         assert(f !is null);
>>>     }
>>>     out (result)
>>>     {
>>>         assert(f.fooWasDone());
>>>         assert(result == true);
>>>     }
>>>     body
>>>     {
>>>         bool fooVal;
>>>         fooVal = f.doFoo();
>>>         return fooVal;
>>>     }
>>>
>>> Note that the in, out, and body are not wrapped in curly braces and that the in and out contracts can't access variables from the body contract (because they are in different scopes), though the in and out contracts can access the arguments and the out contract can also access the return value (as an optional parameter passed to it).  Finally, keep in mind that the in and out contracts (like asserts) aren't included when the compiler is set to release mode so don't put critical error checking in them (they're intended to be used to help verify program correctness while you're developing the program).
>>
>> Actually I know all this, and I've been using it this way. Maybe the
>> example I gave was a bit misleading but what I actualy want to know is if
>> it's possible to use these pre- and postconditions somewhere else then
>> with a function body. Because in the manual they state that with a
>> funtion
>> is "the most typical use", so I'm asking myself what the other uses could
>> be.
>
> Of course there could be other places too. One particularly interesting
> and
> useful feature would be support for contracts in interfaces. From the
> language user's point of view contracts aren't very polished or consistent
> at the moment. Hopefully they will be one of the important features on
> Walter's todo list right after the constness and ast macro stuff.
>
>>
>> Jan
>

Do I understand correct that for the moment contract programming is only possible with functions? But the intention is to extend the possibilities? If not, I'd still like to see al little example.

On Sun, 20 May 2007 12:10:33 +0200, Jan Hanselaer wrote:

> "Jari-Matti Mäkelä" <jmjmak@utu.fi.invalid> schreef in bericht news:f2p10j$fkf$1@digitalmars.com...
>> Jan Hanselaer wrote:
>>
>>>
>>> "Tyler Knott" <tywebmail@mailcity.com> schreef in bericht news:f2ogbj$2kp6$1@digitalmars.com...
>>>> You just got the syntax of the contracts slightly wrong.  This is the correct version:
>>>>
>>>> bool fooFunc(Foo* f)
>>>>     in
>>>>     {
>>>>         assert(f !is null);
>>>>     }
>>>>     out (result)
>>>>     {
>>>>         assert(f.fooWasDone());
>>>>         assert(result == true);
>>>>     }
>>>>     body
>>>>     {
>>>>         bool fooVal;
>>>>         fooVal = f.doFoo();
>>>>         return fooVal;
>>>>     }
>>>>
>>>> Note that the in, out, and body are not wrapped in curly braces and that the in and out contracts can't access variables from the body contract (because they are in different scopes), though the in and out contracts can access the arguments and the out contract can also access the return value (as an optional parameter passed to it).  Finally, keep in mind that the in and out contracts (like asserts) aren't included when the compiler is set to release mode so don't put critical error checking in them (they're intended to be used to help verify program correctness while you're developing the program).
>>>
>>> Actually I know all this, and I've been using it this way. Maybe the
>>> example I gave was a bit misleading but what I actualy want to know is if
>>> it's possible to use these pre- and postconditions somewhere else then
>>> with a function body. Because in the manual they state that with a
>>> funtion
>>> is "the most typical use", so I'm asking myself what the other uses could
>>> be.
>>
>> Of course there could be other places too. One particularly interesting
>> and
>> useful feature would be support for contracts in interfaces. From the
>> language user's point of view contracts aren't very polished or consistent
>> at the moment. Hopefully they will be one of the important features on
>> Walter's todo list right after the constness and ast macro stuff.
>>
>>>
>>> Jan
>>
> 
> Do I understand correct that for the moment contract programming is only possible with functions?

Contract Programming is more than just the 'in', 'out' and 'body' constructs. Those ones are specifically designed for functions though.

The other constructs that go to implementing CP are the 'invariant' and 'assert'. Invariant is specifically designed to work with classes. Assert is designed to work with statements.

In summary ...

'in' is executed before its function is entered.
'out' is executed after its function returns.
'invariant' is executed after /any/ class member function returns.
'assert' is executed whenever statement control flow gets to it.

It sounds like the assert construct is all you need to exercise CP inside a function.


When the documenation say "the most typical use" i think it is referring to why one would be using these constructs not where one would be using them.

> But the intention is to extend the possibilities? If not, I'd still like to see al little example.

void main()
{
   bool assign = false;
   int x;
   assert(assign);
   {x = 1;}
}


I don't believe that 'in' and 'out' can yet be used for nested functions or anonymous functions.

-- 
Derek Parnell
Melbourne, Australia
"Justice for David Hicks!"
skype: derek.j.parnell

Derek Parnell wrote:
> I don't believe that 'in' and 'out' can yet be used for nested functions or
> anonymous functions.

It works fine for nested functions:
---
import std.stdio;

void main()
{
    void nested()
    in {
        writefln("nested : in");
    } out {
        writefln("nested : out");
    } body {
        writefln("nested : body");
    }

    nested();
}
---

You seem to be right about anonymous functions though.

Derek Parnell schrieb am 2007-05-20:


> In summary ...
>
> 'in' is executed before its function is entered.
> 'out' is executed after its function returns.
> 'invariant' is executed after /any/ class member function returns.

'invariant' is executed before and after any public class member function. The only exception are constructors: they don't cause a pre check.

Thomas

It's gone from the documentation, but luckily I've got an old one (this is from DMD 0.176). In the "Contracts" section it was said:

| The in-out statement can also be used inside a function, for example, | it can be used to check the results of a loop:
|
| in
| {
|     assert(j == 0);
| }
| out
| {
|     assert(j == 10);
| }
| body
| {
|     for (i = 0; i < 10; i++)
| 	j++;
| }
|
| This is not implemented at this time.

I guess this is exactly what you want in the example you gave. I don't know why it's gone from the documentation, though. Maybe these feature was dropped from future plans?

Regards,
Ary

Jan Hanselaer escribió:
> Hi
> 
> In the manual http://www.digitalmars.com/d/dbc.html I read  :
> " The pre contracts specify the preconditions before a statement is executed. The most typical use of this would be in validating the parameters to a function. The post contracts validate the result of the statement. The most typical use of this would be in validating the return value of a function and of any side effects it has. "
> Makes sense to me. What I ask myself is if it's useful elsewhere and especially is it possible in D? I tried it with a little example.
> 
> void main()
> {
>    bool assign = true;
>    int x;
>    in{
>       assert(assign);
>    }
>    body{
>       x = 1;
>    }
> }
> 
> 
> It wont compile ("found in instead of statement"). I know it's not exactly a useful example but I just wanted to check if it was possible. I thought it would be because nowhere es said it's not possible. Did I just made a programming error or is it really not possible?
> 
> Greetings
> Jan
> 
> 
> 

Ary Manzana wrote:
> It's gone from the documentation, but luckily I've got an old one (this is from DMD 0.176). In the "Contracts" section it was said:
> 
> | The in-out statement can also be used inside a function, for example, | it can be used to check the results of a loop:
> |
> | in
> | {
> |     assert(j == 0);
> | }
> | out
> | {
> |     assert(j == 10);
> | }
> | body
> | {
> |     for (i = 0; i < 10; i++)
> |     j++;
> | }
> |
> | This is not implemented at this time.
> 
> I guess this is exactly what you want in the example you gave. I don't know why it's gone from the documentation, though. Maybe these feature was dropped from future plans?

Because it wasn't implemented, either it had to be a compiler bug, or removed from the spec. Walter chose the latter. It might come back some day, though.
> 
> Regards,
> Ary