Summary: Some documentation on using Spec# from within C# code.

Using Spec# within a C# project

For various reasons, you may not want to write your code directly in Spec#, but need to use C#. To support this, the Spec# Programming System allows a stylized comment convention in C# code.

The default Spec# console application looks like this in Spec#:

---

		  using System;
	

		  public class Program
		  {
		    static void Main(string![]! args)
		      // The following precondition is redundant with the type
		      // signature for the parameter, but shown here as an example.
		      requires forall{int i in (0:args.Length); args[i] != null};
		    {
		      Console.WriteLine("Spec# says hello!");
		    }
		  }
	

---

In the C# compatibility mode you would write it as:

---

		  using System;
		  //^ using Microsoft.Contracts;
	

		  public class Program
		  {
		    static void Main(string/*!*/[]/*!*/ args)
		      // The following precondition is redundant with the type
		      // signature for the parameter, but shown here as an example.
		      //^ requires forall{int i in (0:args.Length); args[i] != null};
		    {
		      Console.WriteLine("Spec# says hello!");
		    }
		  }
	

---

Everything that Spec# understands, but the C# compiler doesn't has been put into special C# comments. There are three forms:

1. Single line comments

		  //^ Spec# code until the end of the line.
	

2. Multi-line comments

		  /*^ Spec# continues across lines
		       until the end of comment marker.
		  ^*/
	

3. Special non-null comment

		   /*!*/ 
	

It is understood as a shorter (by just a little) than:

		   /*^!^*/
	

(which is also allowed, but requires more characters to type).

All are treated as legal Spec# (by just ignoring the comment marker part when the Spec# compiler processes the source).

In addition, when you installed Spec#, an addition was made to the C# project system. If you look at the Properties page on a C# project, you should see an extra tab "Contracts". On that tab are the options for controlling what the Spec# compiler does with your code. The Spec# compiler is invoked only when you build your project, so you can't get design-time feedback as you do when using the Spec# language service. But if you use the compiler to generate code, then the generated assembly will be the output of the Spec# compiler, not the C# compiler. (The latter's output will be overwritten by the Spec# compiler.) You can also choose whether or not to invoke the static verifier.

Style Hints

You can use the following convention for expose blocks:

		  //^ expose
		  {
		     ... code ...
		  }
	

That way, it is both legal C# and Spec#.

Remember that if you use loop invariants, the body of the loop must be contained in curly braces:

		  foreach(T t in collection)
		    //^ invariant ...
		  {
		     ... code ...
		  }