www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 5023] New: Docs about order of execution of invariant and pre/post conditions

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

           Summary: Docs about order of execution of invariant and
                    pre/post conditions
           Product: D
           Version: D2
          Platform: All
        OS/Version: All
            Status: NEW
          Keywords: spec
          Severity: normal
          Priority: P2
         Component: websites
        AssignedTo: nobody puremagic.com
        ReportedBy: bearophile_hugs eml.cc



This D2 docs page states:
http://www.digitalmars.com/d/2.0/class.html#invariants


 The invariant is checked when a class constructor completes, at the start of
 the class destructor, before a public or exported member is run, and after a
 public or exported function finishes. 



If preconditions, postconditions and invariants are pure functions then they
need to refuse the usage of functions like printf() inside them. If they aren't
pure (maybe because they must support printing and logging), then printing and
logging is a side effect, and their order of execution counts.

Even if preconditions, postconditions and invariants are pure functions, their
purpose is to stop the execution of the program when there's a bug, so during
debugging it's important to know the order of execuction of those contracts, to
understand where the bug is.

Either way, the order of execution of preconditions, postconditions and
invariants is important and it needs to be stated in the D documentation (and
it needs to be the same in different D implementations).

So I suggest to change the D docs like this:


 The invariant is checked when a class constructor completes, at the start of
 the class destructor, before a public or exported member is run (before its
precondition),
 and after a public or exported function finishes (after its postcondition).


-- 
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=5023




See bug 5024

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


Walter Bright <bugzilla digitalmars.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |bugzilla digitalmars.com



13:57:27 PST ---
Fixed, but the order is preconditions, invariant, body, invariant,
postconditions.

-- 
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=5023


Walter Bright <bugzilla digitalmars.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |RESOLVED
         Resolution|                            |FIXED


-- 
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=5023




13:58:09 PST ---
*** Issue 5024 has been marked as a duplicate of this issue. ***

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