Forty Six and Two: July 2010

In this post I’ll show how you can get Code Contracts sort of working for F#. From my very initial explorations, I would conclude that they seem basically usable for F# programming – but you’ll need some glue and tape, and not everything works as you’d expect.

Code Contracts: the short story

Code contracts are a way to express pre- and postconditions and invariants for (theoretically) any CLR based programming language. This is a Very Good Thing, as such contracts are a great way to specify the expected behaviour of your program (i.e. your intent).

Pragmatically, contracts are usually compiled into a debug build of a program, and checked at runtime. That’s how Eiffel does it, where this whole contract thing got started. So every time your program runs, it’s actually being tested in a very deep way. That’s why a tool like Eiffel’s ARTOO, which basically randomly constructs objects and calls method sequences on them, works well: you can find bugs by just executing your program randomly! Of course contracts are also good for documentation: no more looking in the code to find out what happens when you pass in 0 for a particular argument – the pre- and postcondition should tell you.

In the .NET world Code Contracts delivers this kind of functionality by means of a rewriter. That is, you write your actual contracts in a contract language using the System.Diagnostics.Contracts namespace in .NET 4.0, but the methods you’re calling do not actually do much: instead the rewriter runs after the compilation phase on the resulting assembly, recognizes the calls and writes the actual contract checking code in the assembly. This is necessary for example because it’s very useful in a contract to be able to refer to the old value of a parameter, or to the result of the method. Without a rewriter, you’d basically just have something like Debug.Assert, which is not very expressive.

MS research also has made a static checker for contracts, which tries to statically determine whether your contracts hold, and if so, is able to feed that information back to the rewriter so that statically checked contracts do not need to be checked at runtime. Personally I don’t think that is useful because it seems very imprecise. Time will tell – happy to be proven wrong.

Since the rewriter works on the assemblies, you can just use the Contracts API from any .NET language, at least in theory. In practice, different compilers tend to output different representations of types or whatever construct they offer, so it’s not unthinkable that the rewriter gets confused. In fact, in the case of F# it gets confused when you try to write contracts in constructors, as we’ll see.

So while nice in theory, this turns out to be another case of “It works for all .NET languages, as long as they’re exactly like C# or VB.” At least until the contracts folks get round to actually supporting F#, I guess.

The nuts and bolts

‘Nuff complaining. Let’s see how we get code contracts to work with F#.When you install the code contracts add-on, in C# you get a nice extra tab in your project properties. Not so in F# – but that’s the easy part. The whole rewriter thing is actually nicely abstracted away in some custom target file that the Code Contract folks have kindly provided, so we’ll just need some manual editing of the F# project file to get it to work. Here’s an example:

<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
  <PropertyGroup>
    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
    <ProductVersion>8.0.30703</ProductVersion>
    <SchemaVersion>2.0</SchemaVersion>
    <ProjectGuid>{dd086c3a-9cbd-4dc9-89d2-4386df7ee986}</ProjectGuid>
    <OutputType>Exe</OutputType>
    <RootNamespace>CodeContractsFs</RootNamespace>
    <AssemblyName>CodeContractsFs</AssemblyName>
    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
    <Name>CodeContractsFs</Name>
    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
  </PropertyGroup>
  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
    <DebugSymbols>true</DebugSymbols>
    <DebugType>full</DebugType>
    <Optimize>false</Optimize>
    <Tailcalls>false</Tailcalls>
    <OutputPath>bin\Debug\</OutputPath>
    <DefineConstants>TRACE;DEBUG;CONTRACTS_FULL</DefineConstants>
    <WarningLevel>3</WarningLevel>
    <DocumentationFile>bin\Debug\CodeContractsFs.XML</DocumentationFile>
    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
    <CodeContractsCustomRewriterAssembly />
    <CodeContractsCustomRewriterClass />
    <CodeContractsLibPaths />
    <CodeContractsExtraRewriteOptions />
    <CodeContractsExtraAnalysisOptions />
    <CodeContractsBaseLineFile />
    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
  </PropertyGroup>
  <ItemGroup>
    <Reference Include="mscorlib" />
    <Reference Include="FSharp.Core" />
    <Reference Include="System" />
    <Reference Include="System.Core" />
    <Reference Include="System.Numerics" />
  </ItemGroup>
  <ItemGroup>
    <Compile Include="Module1.fs" />
    <None Include="Script.fsx" />
  </ItemGroup>
  <Import Project="$(MSBuildExtensionsPath32)\FSharp\1.0\Microsoft.FSharp.Targets" Condition="!Exists('$(MSBuildBinPath)\Microsoft.Build.Tasks.v4.0.dll')" />
  <Import Project="$(MSBuildExtensionsPath32)\..\Microsoft F#\v4.0\Microsoft.FSharp.Targets" Condition=" Exists('$(MSBuildBinPath)\Microsoft.Build.Tasks.v4.0.dll')" />
</Project>

I’ve put the things to change from a vanilla F# project file in bold. I won’t go over all of them – you can experiment for yourself by playing with the UI in a C# project and checking what the effect is. The three important bits are:

CodeContractsAssemblyMode: per assembly, code contracts allows you to set it in either a compatibility mode (0) or the standard mode (1). For new assemblies, 1 is what you want.
CODECONTRACTS_FULL compile constant: if you don’t define this, the rewriter won’t write the contract checking methods in your assembly. So define this in you Debug configuration (or in a special Contracts configuration)
CodeContractsEnableRuntimeChecking: Otherwise the rewriter doesn’t kick in. Not sure why you’d need this and the constant, but there you go.

Add this to your F# project and you should see the rewriter kick in after the build – it’s called ccrewrite.exe.

Let’s write some contracts

That was the easy part. Now, let’s try to convert the program given in the Code Contracts documentation to F#:

type Rational(numerator,denominator) =
    do Contract.Requires( denominator <> 0 )
    [<ContractInvariantMethod>]
    let ObjectInvariant() = 
        Contract.Invariant ( denominator <> 0 )
    member x.Denominator =
        Contract.Ensures( Contract.Result<int>() <> 0 )
        denominator

So this is a simple rational type. It shows you basically how contracts work – you call methods on the Contract static class:

Contract.Requires to impose a precondition on arguments – in this case an argument of the constructor.
Contract.Ensures to express a postcondition – in this case a postcondition on the result of a getter, which is nicely accessible using Contract.Result.
ObjectInvariantMethodAttribute and Contract.Invariant to impose an invariant on a class – something that should hold after every execution of a method.

So far so good. Alas, when we try to build this, we get:

warning CC1041: Invariant method must be private
error CC1011: This/Me cannot be used in Requires of a constructor
error CC1011: This/Me cannot be used in Requires of a constructor
error CC1011: This/Me cannot be used in Requires of a constructor
error CC1011: This/Me cannot be used in Requires of a constructor
error CC1038: Member 'Module1+Rational.denominator' has less visibility than the enclosing method 'Module1+Rational.#ctor(System.Object,System.Int32)'.: error CC1069: Detected expression statement evaluated for potential side-effect in contracts of method 'Module1+Rational.#ctor(System.Object,System.Int32)'. (Did you mean to put the expression into a Requires, Ensures, or Invariant call?) error CC1004: Malformed contract. Found Requires after assignment in method 'Module1+Rational.#ctor(System.Object,System.Int32)'.

And it turns out that the rewriter is confused by F#’s representation of constructors. When we comment out the Contract.Requires in the constructor, everything works fine.

The warning about the invariant method is because F# actually compiles private members as internal. The rewriter flags this using this warning, but it’s otherwise not much to worry about, I guess, though slightly annoying if you’re – like me – fairly obsessive about getting your code to compile without warnings.

Conclusion

I’ve also checked code contracts with various pre-and postconditions to functions, and that seems to work fine. So overall it’s not a bad story, but it would be nice to see some better integration and to fix the bug(s).

I haven’t checked other features of code contracts, like contract inheritance or expressing code contracts on interfaces, which needs a few tricks as well, so there is a chance that you’ll run into problems there.

Finally, a tip: if you don’t like the C#-ish feel of the Contracts API, you can define your own inline functions that call into the actual API – given that they’re inlined, the rewriter will not see the difference.

So close, but not quite there yet. I’ve asked a year ago if the situation was going to improve, and again a few weeks back, but it’s basically unchanged since then. So F#-ers: head over to the Code Contracts forum and ask for F# support! I’m feeling a bit alone in the desert there at the moment…