F# and contracts in constructors


  • 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)
        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)
        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?


    Sunday, June 14, 2009 9:14 AM

All replies