Contrats de code Analyse statique: Limitations du prouveur?

Question

J'ai joué avec les Contrats de Code et j'aime vraiment ce que j'ai vu jusqu'ici. Ils m'encouragent à évaluer et à déclarer explicitement mes hypothèses, ce qui m'a déjà aidé à identifier quelques cas d'angle que je n'avais pas pris en compte dans le code auquel j'ajoute des contrats. En ce moment je joue avec essayer d'imposer des invariants plus sophistiqués. J'ai un cas qui ne réussit pas actuellement et je suis curieux de savoir s'il y a un moyen de résoudre ce problème, en plus d'ajouter simplement Contract.Assume les appels. Voici la classe en question, dépouillée pour faciliter la lecture:

public abstract class MemoryEncoder 
{ 
    private const int CapacityDelta = 16; 

    private int _currentByte; 

    /// <summary> 
    /// The current byte index in the encoding stream. 
    /// This should not need to be modified, under typical usage, 
    /// but can be used to randomly access the encoding region. 
    /// </summary> 
    public int CurrentByte 
    { 
     get 
     { 
      Contract.Ensures(Contract.Result<int>() >= 0); 
      Contract.Ensures(Contract.Result<int>() <= Length); 
      return _currentByte; 
     } 
     set 
     { 
      Contract.Requires(value >= 0); 
      Contract.Requires(value <= Length); 
      _currentByte = value; 
     } 
    } 

    /// <summary> 
    /// Current number of bytes encoded in the buffer. 
    /// This may be less than the size of the buffer (capacity). 
    /// </summary> 
    public int Length { get; private set; } 

    /// <summary> 
    /// The raw buffer encapsulated by the encoder. 
    /// </summary> 
    protected internal Byte[] Buffer { get; private set; } 

    /// <summary> 
    /// Reserve space in the encoder buffer for the specified number of new bytes 
    /// </summary> 
    /// <param name="bytesRequired">The number of bytes required</param> 
    protected void ReserveSpace(int bytesRequired) 
    { 
     Contract.Requires(bytesRequired > 0); 
     Contract.Ensures((Length - CurrentByte) >= bytesRequired); 

     //Check if these bytes would overflow the current buffer);); 
     if ((CurrentByte + bytesRequired) > Buffer.Length) 
     { 
      //Create a new buffer with at least enough space for the additional bytes required 
      var newBuffer = new Byte[Buffer.Length + Math.Max(bytesRequired, CapacityDelta)]; 

      //Copy the contents of the previous buffer and replace the original buffer reference 
      Buffer.CopyTo(newBuffer, 0); 
      Buffer = newBuffer; 
     } 

     //Check if the total length of written bytes has increased 
     if ((CurrentByte + bytesRequired) > Length) 
     { 
      Length = CurrentByte + bytesRequired; 
     } 
    } 

    [ContractInvariantMethod] 
    private void GlobalRules() 
    { 
     Contract.Invariant(Buffer != null); 
     Contract.Invariant(Length <= Buffer.Length); 
     Contract.Invariant(CurrentByte >= 0); 
     Contract.Invariant(CurrentByte <= Length); 
    } 
} 

Je suis intéressé par la façon dont je peux structurer le contrat appelle à ReserveSpace afin que les invariants de classe sont démontrables. En particulier, il se plaint de (Longueur < = Buffer.Length) et (CurrentByte < = Longueur). Il est raisonnable pour moi qu'il ne puisse pas voir que (Longueur < = Buffer.Length) est satisfait, car il crée un nouveau tampon et réaffecte la référence. Est-ce que ma seule option pour ajouter un suppose que les invariants sont satisfaits?

Answer 1

Après avoir combattu avec pendant un certain temps, je suis venu avec cette solution prouvable (constructeur est un mannequin pour permettre le test isolé):

public abstract class MemoryEncoder 
{ 
    private const int CapacityDelta = 16; 

    private byte[] _buffer; 
    private int _currentByte; 
    private int _length; 

    protected MemoryEncoder() 
    { 
     Buffer = new byte[500]; 
     Length = 0; 
     CurrentByte = 0; 
    } 

    /// <summary> 
    /// The current byte index in the encoding stream. 
    /// This should not need to be modified, under typical usage, 
    /// but can be used to randomly access the encoding region. 
    /// </summary> 
    public int CurrentByte 
    { 
     get 
     { 
      return _currentByte; 
     } 
     set 
     { 
      Contract.Requires(value >= 0); 
      Contract.Requires(value <= Length); 
      _currentByte = value; 
     } 
    } 


    /// <summary> 
    /// Current number of bytes encoded in the buffer. 
    /// This may be less than the size of the buffer (capacity). 
    /// </summary> 
    public int Length 
    { 
     get { return _length; } 
     private set 
     { 
      Contract.Requires(value >= 0); 
      Contract.Requires(value <= _buffer.Length); 
      Contract.Requires(value >= CurrentByte); 
      Contract.Ensures(_length <= _buffer.Length); 
      _length = value; 
     } 
    } 

    /// <summary> 
    /// The raw buffer encapsulated by the encoder. 
    /// </summary> 
    protected internal Byte[] Buffer 
    { 
     get { return _buffer; } 
     private set 
     { 
      Contract.Requires(value != null); 
      Contract.Requires(value.Length >= _length); 
      _buffer = value; 
     } 
    } 

    /// <summary> 
    /// Reserve space in the encoder buffer for the specified number of new bytes 
    /// </summary> 
    /// <param name="bytesRequired">The number of bytes required</param> 
    protected void ReserveSpace(int bytesRequired) 
    { 
     Contract.Requires(bytesRequired > 0); 
     Contract.Ensures((Length - CurrentByte) >= bytesRequired); 

     //Check if these bytes would overflow the current buffer);); 
     if ((CurrentByte + bytesRequired) > Buffer.Length) 
     { 
      //Create a new buffer with at least enough space for the additional bytes required 
      var newBuffer = new Byte[Buffer.Length + Math.Max(bytesRequired, CapacityDelta)]; 

      //Copy the contents of the previous buffer and replace the original buffer reference 
      Buffer.CopyTo(newBuffer, 0); 
      Buffer = newBuffer; 
     } 

     //Check if the total length of written bytes has increased 
     if ((CurrentByte + bytesRequired) > Length) 
     { 
      Contract.Assume(CurrentByte + bytesRequired <= _buffer.Length); 
      Length = CurrentByte + bytesRequired; 
     } 
    } 

    [ContractInvariantMethod] 
    private void GlobalRules() 
    { 
     Contract.Invariant(_buffer != null); 
     Contract.Invariant(_length <= _buffer.Length); 
     Contract.Invariant(_currentByte >= 0); 
     Contract.Invariant(_currentByte <= _length); 
    } 
} 

La principale chose que je remarque est que la mise invariants sur les propriétés se désordre, mais semble résoudre plus facilement avec invariants sur les champs. Il était également important de placer des obligations contractuelles appropriées dans les accesseurs de propriété. Je vais devoir continuer à expérimenter et voir ce qui fonctionne et ce qui ne fonctionne pas. C'est un système intéressant, mais j'aimerais bien en savoir davantage si quelqu'un a une bonne «feuille de triche» sur le fonctionnement du prouveur.