http://d.puremagic.com/issues/show_bug.cgi?id=3856

           Summary: const arguments/instance attributes in
                    conditions/invariants
           Product: D
           Version: 2.040
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: normal
          Priority: P2
         Component: DMD
        AssignedTo: nobody@puremagic.com
        ReportedBy: bearophile_hugs@eml.cc


--- Comment #0 from bearophile_hugs@eml.cc 2010-02-26 13:49:46 PST ---
Currently preconditions and postconditions (D contract based programming) can modify input arguments, this prints [0, 2]:

import std.stdio: writeln;

void foo(int[] arr)
out { arr[0] = 0; }
body {}

void main() {
    auto a = [1, 2];
    foo(a);
    writeln(a);
}

But I think it's better if arguments are seen as const inside preconditions and postconditions. Because modifying them alters too much the program behaviour between release and not release builds.



And I think it's better if instance/static attributes are seen as const inside class/struct invariants:

import std.stdio: writeln;

struct Foo {
    int x;
    invariant() { this.x -= 10; }
    void incr() { x++; }
}

void main() {
    Foo f;
    writeln(f.x);
    f.incr();
    writeln(f.x);
    f.incr();
    writeln(f.x);
}

That code prints different things if compiled in release or not release mode.

----------------------

A small syntactic related problem:

This is correct syntax:
out{}
out(return){}
invariant(){}

This is not valid syntax:
out(){}
invariant{}

I suggest to make such syntax more uniform to help the programmer.

A permissive solution is to allow the following syntax too:
out(){}
invariant{}

Otherwise the syntax:
invariant(){}
Can become, for symmetry with "out":
invariant{}

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=3856



--- Comment #1 from bearophile_hugs@eml.cc 2010-03-01 09:09:00 PST ---
In practice pre/post conditions and invariants can even become pure. This limits some of their usages (logging, printing), but not much.

Generally reading and modifying a global variable inside a condition/invariant doesn't look like tidy code.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=3856


Andrej Mitrovic <andrej.mitrovich@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |andrej.mitrovich@gmail.com


--- Comment #2 from Andrej Mitrovic <andrej.mitrovich@gmail.com> 2010-08-30 06:10:35 PDT ---
(In reply to comment #0)
> Currently preconditions and postconditions (D contract based programming) can modify input arguments, this prints [0, 2]:
> 
> import std.stdio: writeln;
> 
> void foo(int[] arr)
> out { arr[0] = 0; }
> body {}
> 
> void main() {
>     auto a = [1, 2];
>     foo(a);
>     writeln(a);
> }
> 
> But I think it's better if arguments are seen as const inside preconditions and postconditions. Because modifying them alters too much the program behaviour between release and not release builds.
> 

Yes. As stated in TDPL, changing the state of the application inside an in/out contract is *illegal*. An application must run with the same behavior and results whether or not it executes it's contracts (debug vs release mode).

I'm not sure about invariants. Although it would be best if they didn't modify the state of 'this', they are still allowed to call private methods and in turn those methods might change the state of the application.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=3856



--- Comment #3 from bearophile_hugs@eml.cc 2010-10-02 04:30:04 PDT ---
See also bug 4974

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------