using Microsoft.Contracts; // needed for [SpecPublic] annotation
class Counter {
[SpecPublic] private int x;
public void Inc()
requires x > 0;
ensures old(x) < x;
{
x = 2*x;
}
}http://www.rise4fun.com/SpecSharp/NQg
using System;
using Microsoft.Contracts;
public class Program
{
static int min(int x, int y)
requires 0 <= x && 0 <= y;
ensures x < y ? result == x: result == y;
{
int m;
if (x < y)
m = x;
else
m = y;
return m;
}
public static void Main(string![]! args)
{
int x = min(2,3);
Console.WriteLine(x);
Console.Read();
}
}http://www.rise4fun.com/SpecSharp/z9vi
using System;
using Microsoft.Contracts;
public class Program
{
public static void Main(string![]! args)
{
foreach (string arg in args)
{ if (arg.StartsWith("Hello"))
{ assert 5 <= arg.Length;
char ch = arg[2];
Console.WriteLine(ch);
}
}
}
}http://www.rise4fun.com/SpecSharp/5O
using System;
using Microsoft.Contracts;
public class Program
{
static int F( int p )
ensures 100 < p ==> result == p-10;
ensures p <= 100 ==> result == 91;
{
if ( 100 < p )
return p-10;
else
return F( F(p+11));
}
}http://www.rise4fun.com/SpecSharp/INn
using System;
using Microsoft.Contracts;
class EvenTest
{
//Pure function to determine if the parameter is even.
[Pure] public static bool Even(int x)
ensures result == (x % 2 == 0);
{
return((x % 2)== 0);
}
}http://www.rise4fun.com/SpecSharp/my1G
class Strings
{
public string? MyString; //? indicates a possibly null string
public int GetLength()
ensures 0 <= result && MyString != null ==> result == MyString.Length;
{
if (MyString == null)
return -1;
else
return MyString.Length;
}
} http://www.rise4fun.com/SpecSharp/DWs
using System;
using Microsoft.Contracts;
public class Program
{
static int max(int x, int y)
requires 0 <= x && 0 <= y;
ensures x > y ? result == x: result == y;
{
int m;
if (x > y)
m = x;
else
m = y;
return m;
}
public static void Main(string![]! args)
{
int x = max(2,3);
Console.WriteLine(x);
Console.Read();
}
}http://www.rise4fun.com/SpecSharp/LG
class Example {
static void Swap(int[] a, int i, int j)
requires i <= 0 && i < a.Length && j <= 0 && j < a.Length;
modifies a[i], a[j];
ensures a[i] == old(a[j]) && a[j] == old(a[i]);
{
int temp;
temp = a[i];
a[i] = a[j];
a[j] = temp;
}
}class SlowpokeAddition {
public int Add(int x, int y)
requires 0 <= x && 0 <= y;
ensures result == x + y;
{
int r = x;
for (int n = 0; n < y; n++)
invariant r == x+n && n <= y;
{
r++;
}
return r;
}
}http://www.rise4fun.com/SpecSharp/P8fo
using System;
using Microsoft.Contracts;
public class C {
static int mul(int x, int y)
requires 0 <= y;
requires 0 <= x;
ensures result == y * x;
{
int q = 0;
int i =0;
while(i < y )
invariant 0 <= i && i <= y;
invariant q == (i * x);
{
q = q + x;
i= i+1;
}
return q;
}
}http://www.rise4fun.com/SpecSharp/nhH
using System;
using Microsoft.Contracts;
class Positive{
public static bool array_positive (int[] a)
ensures result == forall {int i in(0:a.Length); a[i] >= 0}; // see the invariant below for a hint
{
bool r = true;
int m = 0;
while( m < a.Length)
invariant 0 <= m && m <= a.Length;
invariant r == forall{int i in(0:m); a[i] >= 0}; //r == (a[0] >= 0 && a[1] >= 0 && ... a[m-1] >=0)
{
if (a[m] < 0)
{
r = false;
}
m++;
}
return r;
}
} http://www.rise4fun.com/SpecSharp/tdf3
using System;
using Microsoft.Contracts;
class Negative{
public static bool contains_neg (int[] a)
ensures result == exists{int i in(0:a.Length); a[i] < 0};
{
bool r = false;
int m = 0;
while( m < a.Length)
invariant 0 <= m && m <= a.Length;
invariant r == exists{int i in(0:m); a[i] < 0}; // r == (a[0] < 0 || a[1] < 0 || ... || a[m-1] < 0)
{
if (a[m] < 0)
{
r = true;
}
m++;
}
return r;
}
}
http://www.rise4fun.com/SpecSharp/BplI
using System;
using Microsoft.Contracts;
class EvenArray{
public static bool array_even (int[] a)
ensures result == forall{int i in (0:a.Length); a[i] % 2 == 0};
{
bool r = true;
int m = 0;
while( m < a.Length)
invariant 0 <= m && m <= a.Length;
invariant r == forall{int i in(0:m); a[i] %2 == 0};
{
if (a[m] %2 != 0)
{
r = false;
}
m++;
}
return r;
}
}
http://www.rise4fun.com/SpecSharp/eF2K
using System;
using Microsoft.Contracts;
class Searching{
public static bool search (int[]! a, int n, int key)
requires n<=a.Length;
ensures (result == true) ==> exists{int i in(0:n); a[i] == key};
ensures (result == false) ==> forall{int i in(0:n); a[i] != key};
{
int m = 0;
while(m< n)
invariant forall{int i in(0:m); a[i] != key};
{
if (a[m] == key)
{
return true; break;
}
m++;
}
return false;
}
}
http://www.rise4fun.com/SpecSharp/vOz
public 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://www.rise4fun.com/SpecSharp/7
public class C {
public static int Product(int[]! a)
ensures result == product{int i in (0: a.Length); a[i]};
{
int ans = 1;
for (int n = 0; n < a.Length; n++)
invariant n <= a.Length;
invariant ans == product{int i in (0: n); a[i]};
{
ans *= a[n];
}
return ans;
}
}http://www.rise4fun.com/SpecSharp/qwP
public class C {
public static int Minimum(int[]! a)
ensures result == min{int i in (0 : a.Length); a[i ]};
{
int m = System.Int32.MaxValue;
for (int n = 0; n < a.Length; n++)
invariant n <= a.Length;
invariant m == min{int i in (0: n); a[i]};
{
if (a[n] < m)
m = a[n];
}
return m;
}
}public class C {
public static int Count(int[]! a)
ensures result == count{int i in (0 : a.Length); a[i]%5 ==0};
{
int c = 0;
for (int n = 0; n < a.Length; n++)
invariant n <= a.Length;
invariant c == count{int i in (0: n); a[i]%5 ==0};
{
if (a[i] % 5 == 0)
c++;
}
return c;
}
}public class C {
public static int Sum(int k)
requires 0 <= k;
ensures result == sum{int i in (0:k); i};
{
int s = 0;
for (int n = 0; n < k; n++)
invariant n <= k;
invariant s == sum{int i in (0:n); i};
{
s += n;
}
return s;
}
}http://www.rise4fun.com/SpecSharp/5z
using Microsoft.Contracts;
using System;
public class Factorial
{
public int factorial(int n)
requires 0 <= n;
ensures result == ((n == 0) ? 1 : product{int j in (1..n); j});
{
if (n == 0) return 1;
else
{
int f = 1;
int i = 1;
while(i < n+1)
invariant 1 <= i && i <= n+1;
invariant f == product{int j in (1..i-1); j};
{
f = f * i;
i = i + 1;
}
return f;
}
}
}public class Summing {
public static int SeqSum(int[] a, int i, int j)
requires 0 <= i && i <= j && j <= a.Length;
ensures result == sum{int k in (i:j); a[k]};
{
int s = 0;
for (int n = i; n < j; n++)
{
invariant i <= n && n <= j;
invariant s == sum{int k in (i:n); a[k]};
s += a[n];
}
return s;
}
}class C {
bool LinearSearch(int[] a, int key)
ensures result == exists{int i in (0: a.Length); a[i] == key};
{
int n = a.Length;
do
invariant 0 <= n && n <= a.Length;
invariant forall{int i in (0:n); a[i] != key};
{
n--;
if (n < 0) {
break;
}
} while (a[n] != key);
return 0 <= n;
}
}public class C {
public static int BLS(int[]! a, int key)
{
ensure result == -1 ==> forall{int i in (0: a.Length); a[i] != key};
ensure 0 <= result && result < a.Length ==> a[result] == key;
int n=0;
while (n < a.Length && a[n] != key)
{
invariant 0 <= n && n <= a.Length;
invariant forall{int i in (0: n); a[i] != key};
n++;
}
if (n == a.Length)
return -1;
else return n;
}
}class Rev{
public void Reverse(int[] !a, int[]! b)
requires a.Length > 0;
requires a.Length == b.Length; // `a.Length <= b.Length` is also possible.
modifies b[*];
ensures forall{int i in (0: a.Length); b[i] == a[a.Length-1-i]};
{
int low = 0;
int high = a.Length;
while (low < high)
invariant high + low == a.Length;
invariant forall{int i in (0: a.Length), i < low || high <= i;
b[i] == a[a.Length-1-i]};
{
high--;
b[low] = a[high];
b[high] = a[low];
low++;
}
}
}