Code Contract Mystical [solved]

February 16, 2011  |  .NET, Architecture, Blog, Clean Code, Code Contracts, Contract First  |  4 Comments  |  Share

While struggling to figure out why for my OperationResult constructors the simple precondition:

Contract.Ensures(this.Success == success);

was not verifiable, I finally found the solution changes my OperationResult class as followed.

Code Snippet
//————————————————————————–
// OperationResult.cs” company=”None.”>
//     Copyright (CPOL) 1.02 Theo Jungeblut
//
//     THE WORK (AS DEFINED BELOW) IS PROVIDED UNDER THE TERMS OF THIS CODE
//     PROJECT OPEN LICENSE (“LICENSE”). THE WORK IS PROTECTED BY COPYRIGHT
//     AND/OR OTHER APPLICABLE LAW. ANY USE OF THE WORK OTHER THAN AS
//     AUTHORIZED UNDER THIS LICENSE OR COPYRIGHT LAW IS PROHIBITED.
//
//     BY EXERCISING ANY RIGHTS TO THE WORK PROVIDED HEREIN, YOU ACCEPT
//     AND AGREE TO BE BOUND BY THE TERMS OF THIS LICENSE. THE AUTHOR GRANTS
//     YOU THE RIGHTS CONTAINED HEREIN IN CONSIDERATION OF YOUR ACCEPTANCE OF
//     SUCH TERMS AND CONDITIONS. IF YOU DO NOT AGREE TO ACCEPT AND BE BOUND
//     BY THE TERMS OF THIS LICENSE, YOU CANNOT MAKE ANY USE OF THE WORK.
// </copyright>
// <author>Theo Jungeblut</author>
//————————————————————————–using System;
using System.Collections.Generic;
using System.Collections.ObjectModel;
using System.Diagnostics.Contracts;
using System.Text;namespace Jungeblut.Infrastructure.Common
{
///<summary>
/// Operation Result contains the information about the success of an operation and/or warnings and errors about issues.
///</summary>
[Serializable]
public class OperationResult
{
#region ———————- Fields ———————-
private readonly List<string> errors;
private readonly List<string> warnings;
#endregion

#region ———————- Constructor/Destructor ———————-
///<summary>
/// Initializes a new instance of the OperationResult”/> class for a failed operation.
///</summary>
///<param name=”error”>The error.</param>
public OperationResult(string error)
: this(false, error)
{
Contract.Requires(!string.IsNullOrEmpty(error));
Contract.Ensures(this.Success == false);
Contract.Ensures(this.errors.Contains(error));
}

///<summary>
/// Initializes a new instance of the OperationResult”/> class for an successful operation.
///</summary>
public OperationResult()
: this(true, null)
{
Contract.Ensures(this.Success == true);
}

///<summary>
/// Initializes a new instance of the OperationResult”/> class.
///</summary>
///<param name=”success”>if set to <c>true</c> [success].</param>
///<param name=”message”>Error or Warning message based on Success value.</param>
private OperationResult(bool success, string message)
{
// declare local variables););))
this.errors = new List<string>();
this.warnings = new List<string>();

this.Success = success;

if (!string.IsNullOrEmpty(message))
{
if (this.Success)
{
this.warnings.Add(message);
}
else
{
this.errors.Add(message);
}
}
}
#endregion

#region ———————- Properties ———————-
///<summary>
/// Gets a value indicating whether this OperationResult”/> is success.
///</summary>
///<value>
///<c>true</c> if success; otherwise, <c>false</c>.
///</value>
public bool Success { get; private set; }

///<summary>
/// Gets the errors.
///</summary>
///<value>The errors.</value>
public ReadOnlyCollection<string> Errors
{
get
{
Contract.Ensures(Contract.Result<ReadOnlyCollection<string>>() != null);

return this.errors.AsReadOnly();
}
}

///<summary>
/// Gets the warnings.
///</summary>
///<value>The warnings.</value>
public ReadOnlyCollection<string> Warnings
{
get
{
Contract.Ensures(Contract.Result<ReadOnlyCollection<string>>() != null);

return this.warnings.AsReadOnly();
}
}

#endregion

#region ———————- Public Methods ———————-
#region == operatior
///<summary>
/// Implements the operator ==.
///</summary>
///operationResult1″>The operation result1.</param>
///operationResult2″>The operation result2.</param>
///<returns>The result of the operator.</returns>
public static bool operator ==(OperationResult operationResult1, OperationResult operationResult2)
{
if ((object)operationResult1 == null)
{
return (object)operationResult2 == null;
}

if ((object)operationResult2 == null)
{
return (object)operationResult1 == null;
}

return operationResult1 != null
&& operationResult2 != null
&& operationResult1.Success == operationResult2.Success
&& operationResult1.Errors == operationResult2.Errors
&& operationResult1.Warnings == operationResult2.Warnings;
}

///<summary>
/// Implements the operator ==.
///</summary>
///operationResult”>The operation result.</param>
///<param name=”value”>if set to <c>true</c> [value].</param>
///<returns>The result of the operator.</returns>
public static bool operator ==(OperationResult operationResult, bool value)
{
ValidateContractForEqualOperation(operationResult, value);

return operationResult != null && operationResult.Success == value;
}

///<summary>
/// Implements the operator ==.
///</summary>
///<param name=”value”>if set to <c>true</c> [value].</param>
///operationResult”>The operation result.</param>
///<returns>The result of the operator.</returns>
public static bool operator ==(bool value, OperationResult operationResult)
{
ValidateContractForEqualOperation(operationResult, value);

return operationResult == value;
}
#endregion

#region != operatior
///<summary>
/// Implements the operator !=.
///</summary>
///operationResult1″>The operation result1.</param>
///operationResult2″>The operation result2.</param>
///<returns>The result of the operator.</returns>
public static bool operator !=(OperationResult operationResult1, OperationResult operationResult2)
{
return !(operationResult1 == operationResult2);
}

///<summary>
/// Implements the operator !=.
///</summary>
///operationResult”>The operation result.</param>
///<param name=”value”>if set to <c>true</c> [value].</param>
///<returns>The result of the operator.</returns>
public static bool operator !=(OperationResult operationResult, bool value)
{
return !(operationResult == value);
}

///<summary>
/// Implements the operator !=.
///</summary>
///<param name=”value”>if set to <c>true</c> [value].</param>
///operationResult”>The operation result.</param>
///<returns>The result of the operator.</returns>
public static bool operator !=(bool value, OperationResult operationResult)
{
return !(operationResult == value);
}
#endregion

#region implicit operator bool
///<summary>
/// Performs an implicit conversion from <see cref=”OperationResult”/> to <see cref=”System.Boolean”/>.
///</summary>
///operationResult”>The operation result.</param>
///<returns>The result of the conversion.</returns>
public static implicit operator bool(OperationResult operationResult)
{
Contract.Requires(operationResult != null);

return operationResult.Success;
}
#endregion

#region AddErrorMessage
///<summary>
/// Adds the error message to the errors collection and sets the success value to false if it was true before.
///</summary>
///errorMessage”>The error message.</param>
public void AddErrorMessage(string errorMessage)
{
Contract.Requires(!string.IsNullOrEmpty(errorMessage));
Contract.Ensures(Contract.OldValue<int>(this.errors.Count) + 1 == this.errors.Count);

SetOperationResultToFailed();

this.errors.Add(errorMessage);
}
#endregion

#region AddWarningMessage
///<summary>
/// Adds the warning message to the warnings collection.
///</summary>
///warningMessage”>The warning message.</param>
public void AddWarningMessage(string warningMessage)
{
Contract.Requires(!string.IsNullOrEmpty(warningMessage));
Contract.Ensures(Contract.OldValue<int>(this.warnings.Count) + 1 == this.warnings.Count);

this.warnings.Add(warningMessage);
}
#endregion

#region ToString
///<summary>
/// Returns a string with all errors and warnings, each of them on a separate line starting with all errors.
///</summary>
///<returns>
/// A <see cref=”System.String”/> that represents all errors and warnings.
///</returns>
public override string ToString()
{
Contract.Ensures(Contract.Result<string>() != null);

// declare local variables
StringBuilder stringBuilder;
string warningsAsString;

stringBuilder = new StringBuilder(this.ErrorsToString());

warningsAsString = WarningsToString();
if (!string.IsNullOrEmpty(warningsAsString))
{
if (stringBuilder.Length > 0)
{
stringBuilder.AppendLine();
}

stringBuilder.Append(warningsAsString);
}

return stringBuilder.ToString();
}
#endregion

#region ErrorsToString
///<summary>
/// Returns all errors as a string, where each error message is on a new line.
///</summary>
///<returns>
/// string containing all errors separated with on a new line each
///</returns>
public string ErrorsToString()
{
Contract.Ensures(Contract.Result<string>() != null);

return ListToString(this.Errors);
}
#endregion

#region WarningsToString
///<summary>
/// Returns all warnings as a string, where each error message is on a new line.
///</summary>
///<returns>
/// string containing all warnings separated with on a new line each
///</returns>
public string WarningsToString()
{
Contract.Ensures(Contract.Result<string>() != null);

return ListToString(this.Warnings);
}
#endregion

#region Equals
///<summary>
/// Determines whether the specified <see cref=”System.Object”/> is equal to this instance.
///</summary>
///<param name=”obj”>The <see cref=”System.Object”/> to compare with this instance.</param>
///<returns>
///<c>true</c> if the specified <see cref=”System.Object”/> is equal to this instance; otherwise, <c>false</c>.
///</returns>
public override bool Equals(object obj)
{
return this == (OperationResult)obj;
}
#endregion

#region GetHashCode
///<summary>
/// Returns a hash code for this instance.
///</summary>
///<returns>
/// A hash code for this instance, suitable for use in hashing algorithms and data structures like a hash table.
///</returns>
public override int GetHashCode()
{
return base.GetHashCode();
}
#endregion
#endregion

#region ———————- Private Methods ———————-
#region ListToString
private static string ListToString(IEnumerable<string> list)
{
Contract.Requires(list != null);
Contract.Ensures(Contract.Result<string>() != null);

// declare local variables
StringBuilder stringBuilder;
bool initialExecution;

stringBuilder = new StringBuilder();
initialExecution = true;

foreach (var message in list)
{
if (initialExecution)
{
initialExecution = false;
}
else
{
stringBuilder.AppendLine();
}

stringBuilder.Append(message);
}

return stringBuilder.ToString();
}
#endregion

#region SetOperationResultToFailed
private void SetOperationResultToFailed()
{
Contract.Ensures(this.Success == false);

if (this.Success)
{
this.Success = false;
}
}
#endregion

// Code Contracts helper methods
#region ValidateContractForEqualOperation
[ContractAbbreviator]
private static void ValidateContractForEqualOperation(OperationResult operationResult, bool value)
{
Contract.Ensures((operationResult == null && Contract.Result<bool>() == false)
|| (Contract.Result<bool>() == (operationResult != null && operationResult.Success == value)));
}
#endregion

#region ObjectInvariant
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(this.errors != null);
Contract.Invariant(this.warnings != null);
}
#endregion
#endregion
}
}

 

 

 

By reviewing how I really used the the 3 available constructors I realized that the constructor

public OperationResult(bool success, string message) {…}

was actually never used except from the 2 other constructors, as I always preferred to use the more specialized versions.

As a result, I decided to make this constructor private and removed the preconditions, which where faulty to start with and extremely complex. For the 2 public constructors left, the actual contract with its pre- and post condition  are simple and straight forward.

Summarized I can say by removing unneeded flexibility, I eased my ability to express the correct contract. Isn’t that what clean code is all about?