Invariants for methods

[Jonathan M Davis]

On Thursday 18 November 2010 06:09:33 Jens Mueller wrote:
> Hi,
> 
> I'm wondering what's a good way to do invariants for methods. In my
> example I have a rectangle and one of its methods moves the upper left
> of the rectangle. I have two invariants when moving a rectangle: The
> width and the height do not change. I could do something like the
> following:
> 
> void move(...) {
>     int currentWidth = width;
>     int currentHeight = height;
>     // moving the rectangle here
>     assert(currentWidth == width);
>     assert(currentHeight == height);
> }
> 
> I do not like it because it won't be completely compiled away in release
> mode. The problem is that in the out contract I cannot access variables
> of the in contract. If that was possible it just becomes:
> in {
>     int currentWidth = width;
>     int currentHeight = height;
> }
> out {
>     assert(currentWidth == width);
>     assert(currentHeight == height);
> }
> body {
>     // moving the rectangle here
> }
> 
> Is there a solution that works right now? Are their plans to support
> something like the above? Or should I do it differently?

in blocks define prefix conditions. They can test arguments to the function, 
global variables, and members of the class/struct that the function is a member 
of (if it's a member of one).

out blocks define postfix conditions. They can test the return value of a function 
(assuming that you use out(result) instead of just out), global variables, and 
members of the class/struct that the function is a member of (if it's a member 
of one).

An invariant() block defines an invariant for a class or struct and is called 
before and after every public member function call. It has access to the 
class/struct and global variables (why it requires parens, I don't know).

It makes no sense to talk about an invariant for a function however. All of a 
function's input can be tested with its in block (including global variables and 
member variables if you need to), and all of a function's output can be tested 
with its out block (including global variables and member variables if you need 
to). The only thing left would be checking the function's local variables, but 
they obviously don't exist in the in or out block, and they don't matter outside 
of the function itself. If you care about testing them as you do whatever 
calculations that you're doing in the function, then you can use asserts within 
the function.

The docs page on contracts is here: http://www.digitalmars.com/d/2.0/dbc.html

- Jonathan M Davis