Code Contract Constructor Mystical

February 14, 2011  |  Architecture, Blog, Clean Code, CodeProject, Contract First  |  Share

While preparing my presentation for the Bay.Net User Group which includes the use of Code Contracts I ran into an issue, I try to understand. Below is one of my classes I use in my code example. Within the constructor I make a assignment: this.Success = success; However, somehow is the static analyses  not capable of verifying it. OR I just don’t see what is wrong with my contract specification. Her is the actual source code:

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. ///</summary> ///<param name=”success”>if set to <c>true</c> [success].</param> ///<param name=”message”>Error or Warning message based on Success value.</param> public OperationResult(bool success, string message) { Contract.Ensures(this.Success == success); Contract.Ensures(success == true && !string.IsNullOrEmpty(message) && this.warnings.Contains(message)); Contract.Ensures(success == false && !string.IsNullOrEmpty(message) && this.warnings.Contains(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); Contract.Assume(this.Warnings.Contains(message)); } else { this.errors.Add(message); Contract.Assume(this.Errors.Contains(message)); } } } ///<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); } #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() { // 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 } }

Anyone, wants to jump in and solve the riddle for me?



0 comments