Summary: A way to add contracts to assemblies that were not written in Spec#

Consider mscorlib.dll. Unfortunately it was not written with Spec# and so doesn’t have purity attributes marking any of its methods, and doesn't have any preconditions or postconditions on any of its methods.

To cope with this general problem of not having specifications in 3rd party software, Spec# allows you to have “out-of-band contracts”. An out-of-band contract is a fake assembly that contains just the contracts. The Spec# compiler is able to compile these and doesn’t complain about the missing method bodies. Then, if a client assembly references an out-of-band contract assembly and the real assembly, the Spec# compiler seamlessly glues them together so that it appears as if the real assembly had the contracts all along.

An important point is that the contracts are not injected into the implementation they are a contract for: an out-of-band contract is visible only to clients of the implementation. In the example below, the implementation of A.CallMe is not affected by the contracts contained in the file AC.cs. If you modify the code to break the contract, no contract violation will be reported via the runtime checking. However, if you statically check the contracts with Boogie, then it would report that the implementation fails to live up to its contract.

The Spec# distribution comes with out-of-band contracts for mscorlib.dll and System.dll; Spec# projects using the ''''''VisualStudio project system reference these assemblies by default so you don’t have to even think about it.

Creating your own contract assembly

Here are the steps to produce your own contract assembly. This can be useful if you want to keep your code and contracts completely separate.

1. Compile your non-contract assembly. Let's call it A.dll

2. Write the contracts you want in one or more source files. Let's call this file AC.cs. These files take the form of ordinary Spec# code with contracts, except that method bodies are always omitted (same syntax as abstract methods, i.e., a semicolon after the parameters or the contracts.

3. Compile the contract assembly as follows:

		   ssc /shadow:A.dll /debug /t:library /out:A.Contracts.dll AC.cs
	

Note, we use the convention to name such contract assemblies with a .Contracts.dll suffix, but this is not necessary. However, if you do, the compiler will use them automatically. Otherwise, you have to reference them explicitly.

4. Now you can compile some other code (B.cs) against the A.dll and observe the contracts written in your contract library.

Full example

Below is a minimal example of how this looks. The client code in B.cs uses "null" where a non-null parameter is required. With the contract assembly in place for A.dll, the compiler will issue this warning. Without the contract assembly, the warning will not be emitted.

		 ----Makefile---------------------------------
		 SSC = ssc.exe
	

		 all: A.dll A.Contracts.dll B.exe 
	

		 A.dll: A.cs
		 	$(SSC) /debug /t:library A.cs
	

		 A.Contracts.dll: AC.cs A.dll
	

$(SSC) /debug /t:library /shadow:A.dll /out:A.Contracts.dll AC.cs

		 B.exe: B.cs A.dll A.Contracts.dll
	

$(SSC) /debug /r:A.dll /r:A.Contracts.dll B.cs

		 # Note: the above would work equally well if we omitted the /r:A.Contracts.dll reference
		 #       as the compiler will find this dll due to the naming convention.
	

		 clean:
	

del A.dll A.Contracts.dll B.exe

		 ---Makefile------------------------------------
	

		 ---A.cs----------------------------------------
		 public class A {
		    public int [CallMe(string] s) { return 0; }
		 }
		 ---A.cs----------------------------------------
	

		 ---AC.cs----------------------------------------
		 public class A {
		    public int CallMe(string! s)
		        ensures result >= 0;
		 }
		 ---AC.cs----------------------------------------
	

		 ---B.cs----------------------------------------
		 public class Test {
		    public static void Main() {
	

		        A a = new A();
	

		        [a.CallMe(null);]
		    }
		 }
		 ---B.cs----------------------------------------