Proposal for scoped const contracts

Oliver Dathe o.dathe at gmx.de
Thu Mar 27 15:15:41 PDT 2008


Steven Schveighoffer wrote:
>> Example for syntax (*):
>>
>>     char[] f(char[] p : const(char)[]) { }
>>                 ^               ^
>>    Least restrictive type Tmin  |
>>                      Contract type Tcontract
>> [...]
>> f.) If we want to return some slice of p, we get stuck again. Walter and 
>> Andrei have presented a solution in [2] up to some degree (***).
>>   char[] f(return char[] p : const(char)[]) { return p[17..42]; }
>> g.) f can be virtual, because no templates are required.
> 
> I'm not exactly sure what this accomplishes, because of point f) above, this 
> seems like it is the same as:
> 
> char[] f(const(char)[] p) {...}
> 
> Meaning, f cannot modify p or return a slice of p.

The very first example was just to illustrate the syntax proposal for 
parameter const contracts. The aim is to provide the desired levels of 
const between Tmin and Tcontract. The passed parameter

Imho some more central problem is to apply the const level of the 
parameter (if desired) to the return value. I think in 90% of the time 
this could be solved by Walter/Andreis return storage class (if I got 
that thing right).

Examples:

   char[] f(return char[] p : const(char)[]) {  // p with return&contract
     static if (is(typeof(p)==const(char)[]))
       writefln("const(char)[]");
     else static if (is(typeof(p)==char[]))
       writefln("char[]");
     else
       static assert (false);
     return p[17..42];
   }
   ...
   char[] x = ...;
   auto y = f(x);                               // prints char[]
   static assert (is(typeof(y)==char[]);        // see p's return decl.
   ...
   char[] x = ...;
   auto y = f(cast(const(char)[])x);            // prints const(char)[]
   static assert (is(typeof(z)==const(char)[]); // see p's return decl.
   ...
   const(char)[] x;
   auto y = f(x);                               // prints const(char)[]
   static assert (is(typeof(y)==const(char)[]); // see p's return decl.
   ...
   const(char[]) x;
   auto y = f(x);              // error, f cannot sign the contract
   ...
   void g(int[] p : const(int)[]) {
     p.length = 17;            // ok
     p[42] = '17';             // error, breaks contract, may not compile
   }
   ...
   void h(char[] p const) {...}// short for Tcontract is const(char[])
                               // full contract, p is left invariant by h
   ...
   void i(char[] p) {          // some D1 code, does not know of const
     if (p.length)
       p.length=p.length-1;
   }
   ...
   char[] x = ...;
   i(x const(char)[]);         // call+request4contract => proven&signed
   i(x const(char[]));         // call+request4contract => fails



More information about the Digitalmars-d mailing list