Code Contrat Cheat Sheet

class  CodeContratCheatSheet  {
 
     public int Value { get ; set ; }
         
     [ContractInvariantMethod ]
     private void RationalInvariant(){
 
         Contract .Invariant( this .Value > 0 );
     }
 
     public int VerifyInputParameter(int  a){
             
         Contract .Requires ( (a > 0) && (a < 100) );
         Contract .Ensures  ( a > 0 );
         Contract .Ensures  ( Contract .Result<int >() > 0 );
 
         return  1;
     }
 
     public void VerifyDataInInputOutputParameterOfTypeList(List <int > L){
 
         Contract .Requires( Contract .ForAll( L, l => l > 0 ) );             
         Contract .Ensures ( Contract .ForAll( L, l => l > 0 ) );
     }
 
     public void VerifyOutputParameters(out  int  i){
 
         Contract .Ensures(Contract .ValueAtReturn<int >(out  i) > 0 );
         i=1;
     }
 
     public List <int> VerifyDataInListReturned(){
         Contract .Ensures( Contract .Result<List <int >>().Count > 1 );
         Contract .Ensures(
             Contract .ForAll(
                 0, Contract .Result<List <int >>().Count,
                 index => Contract .Result<List <int >>()[index] > 0
                 )
         );
             
         List <int > l = new  List <int >();
         l.Add(1); l.Add(2); l.Add(3);
         return  l;
     }
 }