I just got it! (invariant/const)

[Georg Wrede]

Jason House wrote:
> Consider this example:
> 
> class D{
>   void invMemberFunc() invariant; // not pure
> }
> 
> class C{
>   int f(invariant D) invariant pure{
>     D.invMemberFunc(); // illegal
>   }
> }

((Upon proofreading it dawned to me that the example above may contain 
errors, but for the sake of clarity, somebody still explain.))

Not being an expert on this stuff, I have to ask:

   void invMemberFunc() invariant; // not pure

What does it actually mean? A function taking no arguments, returning 
nothing? If it has no side effect, then it has no bearing on the 
program, therefore, it essentially is a null function, doing nothing. 
Or, if it has side effects, then the whole question is about: Do we 
allow or disallow pure functions calling member functions with 
intra-object side-effects. (And as far as I understand it, currently 
this is considered illegal, but just may become legal in D3 -- if it 
/really/ then seems like a warranted idea.) (1)

And then it is /invariant/. What exactly does the word invariant mean in 
a function definition when it's after the function name? That it 
requires the argument to be an invariant? (I sure hope it's not some 
property "invariant" of the function, meaning somehow that it doesn't 
change (whatever)).

Along the same lines (please anybody explain),

   int f(invariant D) invariant { ... } //omitting pure here for now

What does that mean? Like, one would understand the latter invariant on 
the line to mean that you only can pass invariant data to the function, 
but then the former invariant on the line would be superfluous, right?

And then,

    int f(invariant D) invariant pure{ ... }

If the function is pure, then should that now implicitly demand an 
invariant argument? (At least as far as I've understood anything about 
this D version.) And therefore actually /both/ invariants are 
superfluous in the definition.

Finally,

> class D{
>   void invMemberFunc() invariant; // not pure
> }
> 
> class C{
>   int f(invariant D) invariant pure{
>     D.invMemberFunc(); // illegal
>   }
> }

Since invMemberFunc is not pure, then using it in f should really be 
illegal. Syntactically, that is, per definition. This because other 
alternatives would be too complicated for the compiler (and the 
programmer) to be practical.

The above example might be clearer (at least to me :-), and depending of 
  course on what exactly you are asking... ) if it said

class D {
   int invMemberFunc(int i) invariant; // not pure
}

class C {
   int e;
   invariant int g;
   int f(invariant D d) invariant pure{
     e = d.invMemberFunc(g); // illegal
   }
}

But again, I'm not expert enough to know for sure what you are asking 
here, so this may not be equivalent.

But, if it were like this, then using invMemberFunc should still be illegal.

---

(1) Which leads to the tought: since a pure function can't call other 
functions to use their side effects, the only reason left to call a 
function is to get it's value. From which follows that calling void 
functions should be made illegal! On the grounds that there is no point 
in calling such a function in the first place. (This as part of the 
"barriers" mentioned in the post 69190 "What is pure and what is not pure".)