You can copy-paste this code directly into the Spec# web-interface. If Spec# gives the message: “Verified, no errors found”, then you're done (of course provided the postcondition is correct).

  class Mult {
    int fi(int x, int y)
      requires x >= 0 && y >= 0;
      ensures result == x * y;
    {
      int r = 0;
      int i = 0;
      while (i < y)
        invariant ... ;
      {
        i = i + 1;
        r = r + x;
      }
      return r;
    }
  }

  class Mult {
    int fi2(int x, int y)
      requires x >= 0 && y >= 0;
      ensures result == x * y;
    {
      int r = 0;
      int i = y;
      while (i > 0)
        invariant ...;
      {
        i = i - 1;
        r = r + x;
      }
      return r;
    }
  }

  class Account {
    private int checkingBalance;
    private int savingsBalance;

    private void checkingDeposit(int amount)
      ensures checkingBalance == old(checkingBalance) + amount;
    {
      checkingBalance = checkingBalance + amount;
    }

    private void checkingWithdraw(int amount)
     ensures checkingBalance == old(checkingBalance) - amount;
    {
      checkingBalance = checkingBalance - amount;
    }

    private void savingsDeposit(int amount)
      ensures savingsBalance == old(savingsBalance) + amount;
    {
      savingsBalance = savingsBalance + amount;
    }
    …
  }

Now add the following two methods to the class above:

  private void transferSavingsToChecking(int amount)
    requires amount > 0 && savingsBalance >= amount;
    ensures savingsBalance == old(savingsBalance) - amount;
    ensures checkingBalance == old(checkingBalance) + amount;
    ensures old(checkingBalance) + old(savingsBalance) == checkingBalance + savingsBalance;
  {
    savingsBalance = savingsBalance - amount;
    checkingBalance = checkingBalance + amount;
  }

  private void transferCheckingToSavings(int amount)
    requires amount > 0 && checkingBalance >= amount;
    ensures old(checkingBalance) + old(savingsBalance) == checkingBalance + savingsBalance;
  {
    checkingWithdraw(amount);
    savingsDeposit(amount);
  }

  class Sqrt {
    public int sqrt(int x)
      requires 0 <= x;
      ensures result*result <= x && x < (result+1)*(result+1);
    {
      int r = 0;
      while ((r+1)*(r+1) <= x)
        invariant ... ;
      {
        r++;
      }
      return r;
    }
  }

  class LinearSearch {
    bool search(int[] a, int key)
      ensures result == exists{int i in (0: a.Length); a[i] == key};
    {
      int n = a.Length;
      do
        invariant ...;
      {
        n--;
        if (n < 0) {
          break;
        }
      } while (a[n] != key);
      return 0 <= n;
    }
  }

  class SomeFunction1 {
    public int f(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;
    }
  }

  class GCD {
    int gcd(int a, int b)
      requires a > 0 && b > 0;
      ensures ...;
      ensures ...;
    {
      int i = 1; int res = 1;
      while (i < a+b)
        invariant ...;
      {
        i++;
        if (a % i == 0 && b % i == 0) {
          res = i;
        }
      }
      return res;
    }
  }