Perché i Contratti di codice sostengono che "Assures è falso" per questo codice?

Question

Questo è un costruttore in una delle mie classi:

public SemanticVersion(string version) 
{ 
    Contract.Requires<ArgumentException>(!string.IsNullOrEmpty(version)); 
    Contract.Ensures(MajorVersion >= 0); 
    Contract.Ensures(MinorVersion >= 0); 
    Contract.Ensures(PatchVersion >= 0); 
    Contract.Ensures(PrereleaseVersion != null); 
    Contract.Ensures(BuildVersion != null); 

    var match = SemanticVersionRegex.Match(version); 
    if (!match.Success) 
    { 
     var message = $"The version number '{version}' is not a valid semantic version number."; 
     throw new ArgumentException(message, nameof(version)); 
    } 

    MajorVersion = int.Parse(match.Groups["major"].Value, CultureInfo.InvariantCulture); 
    MinorVersion = int.Parse(match.Groups["minor"].Value, CultureInfo.InvariantCulture); 
    PatchVersion = int.Parse(match.Groups["patch"].Value, CultureInfo.InvariantCulture); 
    PrereleaseVersion = match.Groups["prerelease"].Success 
     ? new Maybe<string>(match.Groups["prerelease"].Value) 
     : Maybe<string>.Empty; 
    BuildVersion = match.Groups["build"].Success 
     ? new Maybe<string>(match.Groups["build"].Value) 
     : Maybe<string>.Empty; 
} 

i contratti Codice bandiere checker statico un errore:

warning : CodeContracts: ensures is false: PrereleaseVersion != null

Maybe<T> è una raccolta contenente zero o uno elementi.

Per quanto posso vedere, l'unico modo che può essere nullo è se c'è un'eccezione prima che sia assegnata, il che dovrebbe rendere irrilevanti i requisiti di Ensures. Sto andando codice cieco? Riesci a vedere il problema ...?

Aggiornamento: registrazione dell'implementazione di Forse in risposta ai commenti.

using System.Collections; 
using System.Collections.Generic; 
using System.Diagnostics.Contracts; 
using System.Linq; 

namespace TA.CoreTypes 
{ 
    /// <summary> 
    ///  Represents an object that may or may not have a value (strictly, a collection of zero or one elements). Use 
    ///  LINQ expression 
    ///  <c>maybe.Any()</c> to determine if there is a value. Use LINQ expression 
    ///  <c>maybe.Single()</c> to retrieve the value. 
    /// </summary> 
    /// <typeparam name="T">The type of the item in the collection.</typeparam> 
    public class Maybe<T> : IEnumerable<T> 
    { 
     private static readonly Maybe<T> EmptyInstance = new Maybe<T>(); 
     private readonly IEnumerable<T> values; 

     /// <summary> 
     ///  Initializes a new instance of the <see cref="Maybe{T}" /> with no value. 
     /// </summary> 
     private Maybe() 
     { 
      values = new T[0]; 
     } 

     /// <summary> 
     ///  Initializes a new instance of the <see cref="Maybe{T}" /> with a value. 
     /// </summary> 
     /// <param name="value">The value.</param> 
     public Maybe(T value) 
     { 
      Contract.Requires(value != null); 
      values = new[] {value}; 
     } 

     /// <summary> 
     ///  Gets an instance that does not contain a value. 
     /// </summary> 
     /// <value>The empty instance.</value> 
     public static Maybe<T> Empty 
     { 
      get 
      { 
       Contract.Ensures(Contract.Result<Maybe<T>>() != null); 
       return EmptyInstance; 
      } 
     } 

     public IEnumerator<T> GetEnumerator() 
     { 
      Contract.Ensures(Contract.Result<IEnumerator<T>>() != null); 
      return values.GetEnumerator(); 
     } 

     IEnumerator IEnumerable.GetEnumerator() 
     { 
      Contract.Ensures(Contract.Result<IEnumerator>() != null); 
      return GetEnumerator(); 
     } 

     [ContractInvariantMethod] 
     private void ObjectInvariant() 
     { 
      Contract.Invariant(values != null); 
     } 

     [Pure] 
     public override string ToString() 
     { 
      Contract.Ensures(Contract.Result<string>() != null); 
      if (Equals(Empty)) return "{no value}"; 
      return this.Single().ToString(); 
     } 
    } 

    public static class MaybeExtensions 
    { 
     public static bool None<T>(this Maybe<T> maybe) 
     { 
      if (maybe == null) return true; 
      if (maybe == Maybe<T>.Empty) return true; 
      return !maybe.Any(); 
     } 
    } 
} 

Answer 1

Sembra che gli unici metodi mutator sulla classe Maybe<T> sono i costruttori stessi. Ogni altro metodo ottiene solo cose. Pertanto, potresti inserire lo PureAttribute a livello di classe per suggerire all'analizzatore che l'intera classe è pura, dato che è immutabile — dopotutto, non è il punto di un Forse, o ottieni qualcosa, o otterrai un Vuoto Forse , ma non ottieni mai nulla? E non puoi cambiare il valore in un Forse, puoi solo creare un nuovo Forse contenente un nuovo valore.

Inoltre, ho sempre avuto problemi con l'analizzatore statico e utilizzo di Contract.Ensures con proprietà nei costruttori (in particolare, proprietà mutabili), anche con gli invarianti oggetto specificati; Non sono abbastanza sicuro del perché questo sia.

In ogni caso, se si dispone di proprietà immutabili, quindi il codice qui sotto dovrebbe funzionare:

// If this class is immutable, consider marking it with: 
// [Pure] 
public class SemanticVersion 
{ 
    private readonly int _majorVersion; 
    private readonly int _minorVersion; 
    private readonly int _patchVersion; 
    private readonly Maybe<T> _buildVersion; 
    private readonly Maybe<T> _prereleaseVersion; 

    public SemanticVersion(string version) 
    { 
     Contract.Requires<ArgumentException>(!string.IsNullOrEmpty(version)); 

     var match = SemanticVersionRegex.Match(version); 
     if (!match.Success) 
     { 
      var message = $"The version number '{version}' is not a valid semantic version number."; 
      throw new ArgumentException(message, nameof(version)); 
     } 

     _majorVersion = int.Parse(match.Groups["major"].Value, CultureInfo.InvariantCulture); 
     _minorVersion = int.Parse(match.Groups["minor"].Value, CultureInfo.InvariantCulture); 
     _patchVersion = int.Parse(match.Groups["patch"].Value, CultureInfo.InvariantCulture); 
     _prereleaseVersion = match.Groups["prerelease"].Success 
      ? new Maybe<string>(match.Groups["prerelease"].Value) 
      : Maybe<string>.Empty; 
     _buildVersion = match.Groups["build"].Success 
      ? new Maybe<string>(match.Groups["build"].Value) 
      : Maybe<string>.Empty; 
    } 

    [ContractInvariantMethod] 
    private void ObjectInvariants() 
    { 
     Contract.Invariant(_majorVersion >= 0); 
     Contract.Invariant(_minorVersion >= 0); 
     Contract.Invariant(_patchVersion >= 0); 
     Contract.Invariant(_prereleaseVersion != null); 
     Contract.Invariant(_buildVersion != null); 
    } 

    // Properties that only contain getters are automatically 
    // considered Pure by Code Contracts. But also, this point 
    // is moot if you make the entire class Pure if it's 
    // immutable. 
    public int MajorVersion => _majorVersion; 
    public int MinorVersion => _minorVersion; 
    public int PatchVersion => _patchVersion; 
    public Maybe<T> PrereleaseVersion => _prereleaseVersion; 
    public Maybe<T> BuildVersion => _buildVersion; 
} 

Se la classe non è pura e le proprietà sono mutabili, allora avrete bisogno di creare le proprietà che fanno riferimento alla piena privata campi di supporto. Ma lo stesso metodo ObjectInvariants dovrebbe essere abbastanza per strumentare la tua classe con i giusti contratti.

Answer 2

Potrebbe essere null se match.Success è falso.

Prova questo ...

public SemanticVersion(string version) 
{ 
    Contract.Requires<ArgumentException>(!string.IsNullOrEmpty(version)); 
    Contract.Ensures(MajorVersion >= 0); 
    Contract.Ensures(MinorVersion >= 0); 
    Contract.Ensures(PatchVersion >= 0); 
    Contract.Ensures(PrereleaseVersion != null); 
    Contract.Ensures(BuildVersion != null); 

    var match = SemanticVersionRegex.Match(version); 
    if (!match.Success) 
    { 
     // set the values here 
     PrereleaseVersion = Maybe<string>.Empty; 
     BuildVersion = Maybe<string>.Empty; 
     var message = $"The version number '{version}' is not a valid semantic version number."; 
     throw new ArgumentException(message, nameof(version)); 
    } 

    MajorVersion = int.Parse(match.Groups["major"].Value, CultureInfo.InvariantCulture); 
    MinorVersion = int.Parse(match.Groups["minor"].Value, CultureInfo.InvariantCulture); 
    PatchVersion = int.Parse(match.Groups["patch"].Value, CultureInfo.InvariantCulture); 
    PrereleaseVersion = match.Groups["prerelease"].Success 
     ? new Maybe<string>(match.Groups["prerelease"].Value) 
     : Maybe<string>.Empty; 
    BuildVersion = match.Groups["build"].Success 
     ? new Maybe<string>(match.Groups["build"].Value) 
     : Maybe<string>.Empty; 
} 

... Basato su un commento qui è un esempio di stato di essere mutato durning un'eccezione.

class Program 
{ 
    static void Main(string[] args) 
    { 
     var obj = new MyObject() { Prop1 = "Hello", }; 
     Console.WriteLine(obj.Prop1); 
     try 
     { 
      obj.DoWork(); 
     } 
     catch (Exception) 
     { 
     } 
     Console.WriteLine(obj.Prop1); 

     /* 
     Hello 
     World! 
     */ 
    } 

} 
public class MyObject 
{ 
    public string Prop1 { get; set; } 

    public void DoWork() 
    { 
     this.Prop1 = "World!"; 
     throw new Exception(); 
    } 
}