www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 5027] New: Ghost fields for Contract Programming

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



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: -------
Oct 09 2010
next sibling parent d-bugmail puremagic.com writes:
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



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: -------
Nov 19 2010
prev sibling next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5027






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




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: -------
Nov 19 2010