Posts Tagged ‘Contract First’

Silicon Valley Code Camp 2011: Code Contracts and Pex

October 19, 2011  |  Blog, Code Camps, Events, Silicon Valley Code Camp  |  No Comments  |  Share

Here is my “Contract First Development with Microsoft Code Contracts and Microsoft Pex”-presentation from the Silicon Valley Code Camp 2011.

The presentation can also be downloaded directly from the Downloads page, here.

Summited my sessions for the Silicon Valley Code Camp 2011

April 18, 2011  |  Blog, Code Camps, Events, Silicon Valley Code Camp  |  No Comments  |  Share

After being offline for almost a month due to a bigger backyard project, I finally found the time to work out the sessions, I just summited for the SVCC2011 Oct 8th and 9th at Foothill College. The SVCC is free like the years before and an amazing volunteer powered event organized by Peter Keller. Great job Peter!

The session Clean Code session is now strongly focusing on clean code only. It does not include Code Contracts or supportive VS2010 tools anymore to allow a stronger focus and more time for the main subject.

The Contract-First Development session completely focuses on Microsoft Code Contracts and Pex, giving attendees the time needed to really dive into the advantages of using it.

The session overview on the Silicon Valley Code Camp 2011 website:

http://siliconvalley-codecamp.com/Sessions.aspx

Below are the session details with some more links included:

Clean Code – Why writing Clean Code makes us more efficient

Over the lifetime of a product, maintaining the product is actually one – if not the most – expensive area(s) of the overall product costs. Writing clean code can significantly lower these costs. However, writing clean code also makes you more efficient during the initial development time and results in more stable code. You will be presented design patterns and best practices which will make you write better and more easily maintainable code. You will learn how to apply them by using an existing implementation as the starting point of the presentation. Finally, patterns & practices benefits are explained.

This presentation is based on C# and Visual Studio 2010. However, the demonstrated patterns and practice can be applied to every other programming language too.

Contract-First Development with Microsoft Code Contracts and Microsoft Pex

Design by Contract/Programming, or also called Contract-First development with Code Contracts and Pex, is a design/development approach which first defines a contract for class and its methods before implementing it. Since VS2010, by specifying invariants, pre and post conditions for methods with Code Contracts, Microsoft provides the platform support for taking advantage of this programming paradigm. This allows for writing less and cleaner coder, which is easier to read, test, and document.

Pex, like Code Contracts a development out of the Microsoft Research Lab, allows for automatically creating unit tests. By integrating with Code Contracts, many of the needed Unit Tests can be actually generated instead of written manually.

Finally, Code Contracts also integrate tightly with Microsoft Sandcastle, generating more detailed and accurate MSDN style API documentation and utilizing the conditions specified through Code Contracts.

Within this session, I will give an introduction to Contract-First Development, Code Contracts, Pex and Sandcastle, pointing specifically to the advantages while also addressing limitations and risks.

Design by Contract/ Contract-First Development links
http://en.wikipedia.org/wiki/Design_by_contract

Code Contracts links
http://research.microsoft.com/en-us/projects/contracts/
http://www.codeproject.com/KB/cs/CodeContracts.aspx
http://www.codeproject.com/KB/cs/CodeContracts_Pt2.aspx

Pex links
http://research.microsoft.com/en-us/projects/pex/
http://lammichalfranc.wordpress.com/2010/08/15/microsoft-pex-automated-unit-testing/http://blogs.u2u.be/peter/post/2010/04/10/Pex-and-Code-Contracts.aspx

Sandcastle links
http://blogs.msdn.com/b/sandcastle/
http://sandcastle.codeplex.com/

Code Contract Constructor Mystical

February 14, 2011  |  Architecture, Blog, Clean Code, CodeProject, Contract First  |  No Comments  |  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?