Using Code Contracts for Safer Code

FirstBankOfSafety.cs

class FirstBankOfSafety
{
  /// <summary>
  /// The current balance in the account
  /// </summary>
  public double CurrentBalance { get; private set; }
  
  /// <summary>
  /// Deposit money into your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to deposit</param>
  /// <returns>The current balance in the account after the deposit.</returns>
  public double Deposit(double value)
  { //  enforce Rule # 1
    Contract.Requires(value > 0.0, "You must deposit a value greater than $0.00");
    
    //  add the new value to your balance
    CurrentBalance += value;
    
    //  return the current balance
    return CurrentBalance;
  }
  
  /// <summary>
  /// Withdrawal money from your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to withdrawal</param>
  /// <returns>The current balance in the account after the widthdrawal</returns>
  public double Withdrawal(double value)
  { //  enforce Rule # 3
    Contract.Requires(value <= CurrentBalance, "No withdrawal can be greater than the current balance.");
    Contract.Requires(value > 0.0, "You cannot withdrawal a negative value.");
    
    //  remove the value from the current balance
    CurrentBalance -= value;
    
    //  return the current balance
    return CurrentBalance;
  }
}

FirstBankOfSloppyness.cs

class FirstBankOfSloppyness
{
  /// <summary>
  /// The current balance in the account
  /// </summary>
  public double CurrentBalance { get; private set; }

  /// <summary>
  /// Deposit money into your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to deposit</param>
  /// <returns>The current balance in the account after the deposit.</returns>
  public double Deposit(double value)
  { //  add the new value to your balance
    CurrentBalance += value;
    
    //  return the current balance
    return CurrentBalance;
  }
  
  /// <summary>
  /// Withdrawal money from your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to withdrawal</param>
  /// <returns>The current balance in the account after the widthdrawal</returns>
  public double Withdrawal(double value)
  { //  remove the value from the current balance
    CurrentBalance -= value;
    
    //  return the current balance
    return CurrentBalance;
  }
}

SampleWithoutAssertions.cs

private static void SampleWithoutAssertions()
{
  var bank = new FirstBankOfSloppyness();
  
  Console.WriteLine("[SloppyBank] Starting Balance: {0,8:c}", bank.CurrentBalance);
  
  bank.Deposit(100.0);
  Console.WriteLine("[SloppyBank] Balance After Depositing $100.00: {0,8:c}", bank.CurrentBalance);
  
  bank.Deposit(100.0);
  Console.WriteLine("[SloppyBank] Balance After Depositing $100.00: {0,8:c}", bank.CurrentBalance);
  
  bank.Deposit(-500.0);
  Console.WriteLine("[SloppyBank] Balance After Depositing -$500.00: {0,8:c}", bank.CurrentBalance);
  
  bank.Deposit(1500.0);
  Console.WriteLine("[SloppyBank] Balance After Depositing $1500.00: {0,8:c}", bank.CurrentBalance);
  
  bank.Withdrawal(5000.0);
  Console.WriteLine("[SloppyBank] Balance After Depositing $1500.00: {0,8:c}", bank.CurrentBalance);
}

SecondBankOfSafety.cs

class SecondBankOfSafety
{
  /// <summary>
  /// The current balance in the account
  /// </summary>
  public double CurrentBalance { get; private set; }
  
  /// <summary>
  /// Deposit money into your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to deposit</param>
  /// <returns>The current balance in the account after the deposit.</returns>
  public double Deposit(double value)
  { //  enforce Rule # 1
    Contract.Requires(value > 0.0, "You must deposit a value greater than $0.00");
    //  enforce Rule # 2
    Contract.Ensures(CurrentBalance >= 0);
    
    //  add the new value to your balance
    CurrentBalance += value;
    
    //  return the current balance
    return CurrentBalance;
  }
  
  /// <summary>
  /// Withdrawal money from your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to withdrawal</param>
  /// <returns>The current balance in the account after the widthdrawal</returns>
  public double Withdrawal(double value)
  { //  enforce Rule # 3
    Contract.Requires(value <= CurrentBalance, "No withdrawal can be greater than the current balance.");
    Contract.Requires(value > 0.0, "You cannot withdrawal a negative value.");
    //  enforce Rule # 2
    Contract.Ensures(CurrentBalance >= 0);
    
    //  remove the value from the current balance
    CurrentBalance -= value;
    
    //  return the current balance
    return CurrentBalance;
  }
}

ThirdBankOfSafety.cs

class ThirdBankOfSafety
{
  /// <summary>
  /// The current balance in the account
  /// </summary>
  public double CurrentBalance { get; private set; }
  
  [ContractInvariantMethod]
  private void ThirdBankOfSafetyInvariant()
  { //  enforce Rule # 2
    Contract.Invariant(CurrentBalance >= 0, "The balance must be greater than or equal to $0.00");
  }
  /// <summary>
  /// Deposit money into your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to deposit</param>
  /// <returns>The current balance in the account after the deposit.</returns>
  public double Deposit(double value)
  { //  enforce Rule # 1
    //Contract.Requires(value > 0.0, "You must deposit a value greater than $0.00");
    
    //  add the new value to your balance
    CurrentBalance += value;
    
    //  return the current balance
    return CurrentBalance;
  }
  
  /// <summary>
  /// Withdrawal money from your bank account and return the new balance
  /// </summary>
  /// <param name="value">The amount to withdrawal</param>
  /// <returns>The current balance in the account after the widthdrawal</returns>
  public double Withdrawal(double value)
  { //  enforce Rule # 3
    //Contract.Requires(value <= CurrentBalance, "No withdrawal can be greater than the current balance.");
    Contract.Requires(value > 0.0, "You cannot withdrawal a negative value.");
    
    //  remove the value from the current balance
    CurrentBalance -= value;
    
    //  return the current balance
    return CurrentBalance;
  }
}