www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 5024] New: Order of execution of invariant and pre/post conditions

reply d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5024

           Summary: Order of execution of invariant and pre/post
                    conditions
           Product: D
           Version: D2
          Platform: x86
        OS/Version: Windows
            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-10-09 06:36:30 PDT ---
This is a D2 program that uses Contracts:


import std.c.stdio: printf;

class Foo {
    int x = 0;

    invariant() {
        printf("Foo invariant: %d\n", x);
        assert(x >= 0);
    }

    this() {
        printf("Foo constructor: %d\n", x);
        x = 0;
    }

    void setX(int newx)
        in {
            printf("Foo.setX precondition: %d\n", newx);
            assert(newx >= 0);
        } out {
            printf("Foo.setX postcondition: %d\n", x);
            assert(x == newx);
        } body {
            printf("Foo.setX body\n");
            x = newx;
        }
}

void main() {
    auto c = new Foo();
    c.setX(10);
}


This is the output of the program, DMD 2.049:

Foo constructor: 0
Foo invariant: 0
Foo.setX precondition: 10
Foo invariant: 0
Foo.setX body
Foo invariant: 10
Foo.setX postcondition: 10


But I think the Foo.setX precondition needs to run after the Foo invariant, and
the Foo.setX postcondition has to run before the Foo invariant.

See bug 5023

See also bug 3578 and bug 3856

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
Oct 09 2010
next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5024


Walter Bright <bugzilla digitalmars.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |RESOLVED
                 CC|                            |bugzilla digitalmars.com
         Resolution|                            |DUPLICATE


--- Comment #1 from Walter Bright <bugzilla digitalmars.com> 2012-01-19
13:58:09 PST ---
*** This issue has been marked as a duplicate of issue 5023 ***

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
Jan 19 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5024



--- Comment #2 from bearophile_hugs eml.cc 2012-01-19 19:25:11 PST ---
It's not a duplicate. Issue 5023 asks to document something, and this issue
asks to make that something in a different way.

A discussion thread:
http://www.digitalmars.com/webnews/newsgroups.php?art_group=digitalmars.D&article_id=155592

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
Jan 19 2012
prev sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5024



--- Comment #3 from bearophile_hugs eml.cc 2012-01-19 19:28:04 PST ---
Walter has said:

 My reasoning is it (1) doesn't make any difference and (2) it's always
 been like that - and if it did make a difference, it would break 10 years
 of existing code.
A note: this issue is of a list of about twenty issues that I especially care about. Essentially *all* of them are little/tiny breaking changes like this one. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email ------- You are receiving this mail because: -------
Jan 19 2012