RiSE4fun samples for Code ContractsList of built-in samples for the Code Contracts in RiSE4funen-US<a target='_blank' href='https://go.microsoft.com/?linkid=2028325'>Contact Us</a>| <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=521839'>Privacy &amp; Cookies</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkID=246338'>Terms of Use</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=506942 '>Trademarks</a>| &copy; 2017 Microsofthttps://rise4fun.com//Images/Rise.gifRiSE4fun samples for Code Contractshttps://rise4fun.com/CodeContracts/AbsAbsusing System; using System.Diagnostics.Contracts; class AbsDemo { // Will this method always return a positive value? static int Abs(int i) { Contract.Ensures(Contract.Result<int>() >= 0); // The tool will also suggest a further postcondition // Is this expression doing what you expect? return i > 0 ? i : -i; } } https://rise4fun.com/CodeContracts/MaxMaxusing System; using System.Collections.Generic; using System.Linq; using System.Text; class MaxDemo { // See what the CodeContracts static checker can infer! public static int Max(int[] arr) { var max = arr[0]; for (var i = 1; i < arr.Length; i++) { var el = arr[i]; if (el > max) max = el; } return max; } } https://rise4fun.com/CodeContracts/BinarySearchBinarySearchusing System; using System.Collections.Generic; using System.Linq; using System.Text; using System.Diagnostics.Contracts; class BinarySearchDemo { static int BinarySearch(int[] array, int value) { Contract.Requires(array != null); var inf = 0; var sup = array.Length; // wrong initialization while (inf <= sup) { var index = (inf + sup) / 2; // possible overflow, do you know how to fix it? var mid = array[index]; if (value == mid) return index; if (mid < value) inf = index + 1; else sup = index - 1; } return -1; } }https://rise4fun.com/CodeContracts/HelloWorldHelloWorldusing System; using System.Diagnostics.Contracts; class HelloWorld { // We know args is not-null (implicit Requires of entry point) // But we don't know the number of elements, so we suggest a precondition static void Main(string[] args) { Hello(args[0]); } static void Hello(string name) { Console.WriteLine("Hello {0}", name); } static void FixedMain(string[] args) { Contract.Requires(args != null); // here because this is not an entry point if (args.Length >= 1) Hello(args[0]); else Console.WriteLine("usage: hello [name]"); } } https://rise4fun.com/CodeContracts/ResizeResizeusing System; using System.Collections.Generic; using System.Linq; using System.Text; using System.Diagnostics.Contracts; class ResizeDemo { [ContractInvariantMethod] private void ObjectInvariant() { Contract.Invariant(this.elements != null); Contract.Invariant(this.count >= 0); Contract.Invariant(this.count <= this.elements.Length); } // Something is wrong in this method? // Can you find what? // How should you fix it? public void Add(int x) { if (count == this.elements.Length) { var newElements = new int[count * 2]; Array.Copy(this.elements, newElements, this.elements.Length); this.elements = newElements; } this.elements[count++] = x; } private int count; private int[] elements; public ResizeDemo(int size0) { this.elements = new int[size0]; this.count = 0; } }