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

           Summary: Ghost fields for Contract Programming
           Product: D
           Version: D2
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: enhancement
          Priority: P2
         Component: DMD
        AssignedTo: nobody@puremagic.com
        ReportedBy: bearophile_hugs@eml.cc


--- Comment #0 from bearophile_hugs@eml.cc 2010-10-09 11:51:15 PDT ---
In Design By Contract, (beside the "old" that allows to refer to the state at the entry to the instance method), "ghost fields" (sometimes called 'resources') are sometimes useful. They are auxiliary instance/static attributes that can be read and written only inside pre/post-conditions and invariants. When contracts are disabled, such ghost fields vanish.

Such ghost fields can't be accessed inside static or instance methods of the class/struct/union, so they can't influence the semantics of the class/struct/union (they increase the struct size, so they may change padding too. In structs it's better to put instance ghost fields at the end of the struct, the compiler may even enforce this).

An attribute may be used to define a ghost field, few possible names:

@ghost static int x;
@dbc int x;
@contract int x;
@contracts int x;
@resource int x;
@pro_contract int x;
@pro_contracts static int x;
@just_contract int x;
@contracts_only int x;
@contract_field int x;
@contracts_field static int x;
@dbc_field int x;


The ghost fields may be used to store partial computations useful to reduce the work done by the class invariant. A disadvantage of ghost fields is that they may make harder the automatic static analysis of Contracts.

A class invariant that modifies ghost fields can't be pure. Currently D contracts aren't pure.

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


Bruno Medeiros <bdom.pub+deebugz@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |bdom.pub+deebugz@gmail.com


--- Comment #1 from Bruno Medeiros <bdom.pub+deebugz@gmail.com> 2010-11-19 09:36:07 PST ---
Or alternatively, have the compiler define a debug/version identifier when compiled in release mode, and then just use conditional compilation.

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



--- Comment #2 from bearophile_hugs@eml.cc 2010-11-19 09:45:30 PST ---
(In reply to comment #1)
> Or alternatively, have the compiler define a debug/version identifier when compiled in release mode, and then just use conditional compilation.

In that case the compiler can't enforce this constraint:

> can't be accessed inside static or instance methods of the class/struct/union,

The idea is that ghost field may be read/written only inside pre/post-conditions and invariants.

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



--- Comment #3 from Bruno Medeiros <bdom.pub+deebugz@gmail.com> 2010-11-19 15:11:32 PST ---
If instead of:

@ghost static int x;

you have:

debug(contracts) static int x;

and "contracts" is said identifier that is only defined in non-release mode, then the compiler can enforce those constraints equally well: Just compile it in release and see if it compiles without errors or not. It might be a minor drawback in compiling performance (if you need to compile twice), but it is not any less of a drawback on compiler checking power.

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