RiSE4fun samples for Spec#List of built-in samples for the Spec# in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Spec#http://rise4fun.com/SpecSharp/IncIncclass Example { int x; void Inc(int y) ensures old(x) < x; { x += y; } } http://rise4fun.com/SpecSharp/AddAddclass SlowpokeAddition { public int Add(int x, int y) requires 0 <= x && 0 <= y; ensures result == 2*x + y; { int r = x; for (int n = 0; n < y; n++) invariant r == x+n && n <= y; { r++; } return r; } } http://rise4fun.com/SpecSharp/SumSumpublic class C { public static int Sum(int[] a) ensures result == sum{int i in (0: a.Length); a[i]}; { int s = 0; for (int n = 0; n <= a.Length; n++) invariant n <= a.Length; invariant s == sum{int i in (0: n); a[i]}; { s += a[n]; } return s; } } http://rise4fun.com/SpecSharp/BinarySearchBinarySearchpublic class C { public static int BinarySearch(int[] a, int key) requires forall{int i in (0: a.Length), int j in (i: a.Length); a[i] <= a[j]}; ensures 0 <= result ==> a[result] == key; ensures result < 0 ==> forall{int i in (0: a.Length); a[i] != key}; { int low = 0; int high = a.Length; while (low < high) invariant 0 <= low && high <= a.Length; invariant forall{int i in (0: low); a[i] != key}; invariant forall{int i in (high: a.Length); a[i] != key}; { int mid = low + (high - low) / 2; int midVal = a[mid]; if (key < midVal) { low = mid + 1; } else if (midVal < key) { high = mid; } else { return mid; // key found } } return -low - 1; // key not found. } } http://rise4fun.com/SpecSharp/ChunkerChunker// This example shows many of the features of Spec#, including pre- // and postcondition of methods and object invariants. The basic // idea in the example is to implement a "chunker", which returns // successive portions of a given string. The main work is done // in the NextChunk() method. // For a full demo showing this example, check out the "The Chunker" // episode on Verification Corner // (http://research.microsoft.com/verificationcorner) public class Chunker { string src; int ChunkSize; invariant 0 <= ChunkSize; int n; // the number of characters returned so far invariant 0 <= n; public string NextChunk() ensures result.Length <= ChunkSize; { string s; if (n + ChunkSize <= src.Length) { s = src.Substring(n, ChunkSize); } else { s = src.Substring(n); } return s; } public Chunker(string source, int chunkSize) { src = source; ChunkSize = chunkSize; n = 0; } } http://rise4fun.com/SpecSharp/BagBagusing System; using Microsoft.Contracts; public sealed class Bag { [Rep] int[] elems; public int Count; invariant 0 <= Count && Count <= elems.Length; public Bag(int[] initialElements) { Count = initialElements.Length; int[] e = new int[initialElements.Length]; Array.Copy(initialElements, 0, e, 0, initialElements.Length); elems = e; } public Bag(int[] initialElements, int start, int howMany) requires 0 <= start && 0 <= howMany; requires start + howMany <= initialElements.Length; { Count = howMany; int[] e = new int[howMany]; Array.Copy(initialElements, start, e, 0, howMany); elems = e; } public int RemoveMin() { int m = System.Int32.MaxValue; int mindex = 0; for (int i = 0; i < Count; i++) invariant 0 <= mindex; { if (elems[i] < m) { mindex = i; m = elems[i]; } } expose (this) { // allow the object invariant to be temporarily violated Count--; elems[mindex] = elems[Count]; } return m; } public void Add(int x) { expose (this) { // allow the object invariant to be temporarily violated if (Count == elems.Length) { int[] b = new int[2*elems.Length]; Array.Copy(elems, 0, b, 0, elems.Length); elems = b; } elems[Count] = x; Count++; } } }