none
F# and contracts in constructors

    Question

  • Hi,

    Although there seems to be no support for it (and pretty much no information...?) I thought I'd get started with using code contracts in F#. Initial experience was good: I just needed to copy some xml tags over from a csproj to an fsproj, define the compilation symbol and the contract checker kicked in.

    But when using preconditions in constructors:

    type Rational (numerator:int,denominator:int) =
        do Contract.Requires( denominator <> 0 ) // <-- here is the problem
        member x.Denominator =
            Contract.Ensures( Contract.Result() <> 0)
            denominator;
    
        [<ContractInvariantMethod>]
        member x.ObjectInvariant() =
            Contract.Invariant(  denominator <> 0 )
    The rewriter fails with:

    EXEC(0,0): error : Detected assignment in a pure region in method 'Module1+Rational.#ctor(System.Int32,System.Int32)'.

    I've also tried F# explicit constructor syntax (that's the first time I ever used it - it is considerably less used in F# programming):

    type RationalEx =
        val numerator:int
        val denominator:int
        new (num:int,denom:int) = 
            {   numerator = num;
                denominator = denom } then Contract.Requires( denom <> 0 ) //<- now here
    
        member x.Denominator =
            Contract.Ensures( Contract.Result() <> 0)
            x.denominator;
    
        [<ContractInvariantMethod>]
        member x.ObjectInvariant() =
            Contract.Invariant(  x.denominator <> 0 )
    But this gives the same error.
    Removing the Ensures in the constructor works nicely. It seems related to previous problems related to VB structs and such?

    thanks,

    Kurt
    Sunday, June 14, 2009 9:14 AM

All replies