www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.learn - contract programming without a function

reply "Jan Hanselaer" <jan.hanselaer gmail.com> writes:
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
May 19 2007
next sibling parent reply Tyler Knott <tywebmail mailcity.com> writes:
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).
May 19 2007
parent reply "Jan Hanselaer" <jan.hanselaer gmail.com> writes:
"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
May 20 2007
next sibling parent reply Jari-Matti =?ISO-8859-1?Q?M=E4kel=E4?= <jmjmak utu.fi.invalid> writes:
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
May 20 2007
parent reply "Jan Hanselaer" <jan.hanselaer gmail.com> writes:
"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.
May 20 2007
parent reply Derek Parnell <derek psych.ward> writes:
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
May 20 2007
next sibling parent reply Frits van Bommel <fvbommel REMwOVExCAPSs.nl> writes:
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.
May 20 2007
parent reply Bruno Medeiros <brunodomedeiros+spam com.gmail> writes:
Frits van Bommel wrote:

 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.


It works fine for anonymous functions too:
----
void main(char[][] args) {
     function void ()
     in {
         writefln("nested : in");
     } out {
         writefln("nested : out");
     } body {
         writefln("nested : body");
     } ();
	
	writeln("END");
}
----
One just is not able to use the shortened anonymous function syntax.

-- 
Bruno Medeiros - MSc in CS/E student
http://www.prowiki.org/wiki4d/wiki.cgi?BrunoMedeiros#D
May 26 2007
parent Frits van Bommel <fvbommel REMwOVExCAPSs.nl> writes:
Bruno Medeiros wrote:

 Frits van Bommel wrote:

 Derek Parnell wrote:

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






[snip nested function counterexample]

 You seem to be right about anonymous functions though.


 
 It works fine for anonymous functions too:
 ----
 void main(char[][] args) {
     function void ()
     in {
         writefln("nested : in");
     } out {
         writefln("nested : out");
     } body {
         writefln("nested : body");
     } ();
     
     writeln("END");
 }
 ----
 One just is not able to use the shortened anonymous function syntax.


Ah, I forgot to try the more explicit form. Good catch.
(Though the fact it took almost a week for someone to post this would 
seem to indicate that not many people were aware of this fact...)
May 26 2007
prev sibling parent Thomas Kuehne <thomas-dloop kuehne.cn> writes:
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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

-----BEGIN PGP SIGNATURE-----

iD8DBQFGUGf3LK5blCcjpWoRAistAKCaoaWOAeGiByk/kYizvNJ2DNQvrQCfXpyL
A/SDQC7J0Xm1gFTNZJqdNTY=
=PEWR
-----END PGP SIGNATURE-----
May 20 2007
prev sibling parent BCS <ao pathlink.com> writes:
Reply to Jan,


 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
 


other uses would be logging

void foo(int i)
in{writef(">foo(%d)\n", i);}
out{writef("<foo()\n");}
May 20 2007
prev sibling parent reply Ary Manzana <ary esperanto.org.ar> writes:
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
May 20 2007
next sibling parent Don Clugston <dac nospam.com.au> writes:
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
May 20 2007
prev sibling parent reply BCS <ao pathlink.com> writes:
Reply to Ary,


 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?
 


you can fake this with scope(exit)


|assert(j == 0);
|{
|    scope(exit) assert(j == 10);
|    for (i = 0; i < 10; i++)
|        j++;
|}
May 20 2007
parent Ary Manzana <ary esperanto.org.ar> writes:
BCS escribió:

 
 you can fake this with scope(exit)
 
 
 |assert(j == 0);
 |{
 |    scope(exit) assert(j == 10);
 |    for (i = 0; i < 10; i++)
 |        j++;
 |}


Almost. If your "in" or "out" bodies have statements that are not 
exclusively asserts, then they won't be gone when compiling in release mode.

The following would also be nice (althugh I seriosuly doubt people will 
use it):

| for(int i = 0; i < 10; i++) {
|     invariant {
|        assert(0 >= i && i < 10);
|     }
|     // some code...
| }

Here again, the invariant may contain code that is not exclusively 
assert, so in release mode it will be gone. And it's much nicer to the eye.
May 21 2007