www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 3856] New: const arguments/instance attributes in conditions/invariants

reply d-bugmail puremagic.com writes:
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



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: -------
Feb 26 2010
next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=3856




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: -------
Mar 01 2010
prev sibling next sibling parent d-bugmail puremagic.com writes:
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



06:10:35 PDT ---


 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: -------
Aug 30 2010
prev sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=3856




See also bug 4974

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