Bug 5027 – Ghost fields for Contract Programming

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.

Or alternatively, have the compiler define a debug/version identifier when compiled in release mode, and then just use conditional compilation.

(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.

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.

Since this is a significant proposal, it should be a DIP. Refer to https://github.com/dlang/DIPs/ if you want to pursue this.