Summary: Ghost fields for Contract Programming
           Product: D
           Version: D2
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: enhancement
          Priority: P2
         Component: DMD

--- Comment #0 from 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:
------- You are receiving this mail because: -------

Reply via email to