Code Contract (Language Support)

Topics: C# Language Design, VB Language Design
Aug 14, 2014 at 8:52 AM

Code Contract (Language Support)

Suppose Code Contracts were explicitly embedded into the language definitions of c# and vb.net.
How could it potentially look? Note: contracts for return (or yield) parameters not yet implemented in this version of the design.

A method parameter that as a contract associated with is post-fixed with a # digit+
Note: Think like a footnote marker in written texts

Examples

C# ( int32 xx = 0 #0 , ... vb.net ( xx As Int32 = 0 #0 , ...

Basic Structure

The basic structure of the contract code.
/* C# */
         Digit ::= '0' - '9'
    ElseClause ::= 'else' ContractExpr 
ContractClause ::= '[' Digit+ ']' '{' ContractExpr '}' ElseClause?
      Contract ::= 'Contract' '{' ContractClause* '}'
/* vb.net */
         Digit ::= '0' - '9'
    ElseClause ::= ' Else ' ContractExpr 
ContractClause ::= 'Clause ' Digit+ ' : ' ContractExpr ElseClause?
      Contract ::= 'Contract'
                      ContractClause*
                   'End Contract'
The use of ContractExpr allow the set of allow expression to be restricted or even be an embedded domain specific language designed for contracts.

Layout

The contract block is placed after the method signature and before the code body of the method
C#
method ( Int32 arg #0 )
   contract 
   {
     /* body of contract */
    [ 0 ] { /* body of clause */ } else { /* body of else clause */ }
   }
{
 /* body of method */
} 

__VB.net
Sub method ( Arg0 As Int32 #0 )
  Contract
    Clause 0 : 
    ' Clause Body
    Else
    ' Else Clause Body 
  End Contract
End Sub
note It also possible to write to clause as on a single line in vb.net
Clause 0: clause_body Else else_clause_body

Examples

C#
object Foo< T : class > ( T Arg0 #0, Int32 Arg1 #1, Int32 Arg2 #2)
  contract { [0]{ { Arg0 IsNot Null } else { Arg0 = T.Default } }
             [1]{ { [ 0 <= Arg1 < XMax ] } else { } } /* IsBetween ContractExpr */
             [2]{ { [ 0 <= Arg2 < YMax ] } else { } }
           }
{
  /* code body of method */
} 
vb.net
Function Foo (Of T As Class) ( Arg0 As T #0,
                               Arg1 As Int32 #1,
                               Arg2 As Int32 #2 
                             ) As Object
  Contract
     Clause 0 : Arg0 IsNot Nothing Else Arg0 = T.Default
     Clause 1 : [ 0 <= Arg1 < XMax ] 
     Clause 2 : [ 0 <= Arg2 < YMax ]
  End Contract

  ' -- Code Body of Method --
End Function

vb.net
Default Property Item ( Index As Integer #0 ) As T
  ' -- Contract is applicable to both getter and setter -- '
  Contract
    Clause 0: [ 0 <= Index < ItemCount ]  
  End Contract
  
  Get
    Return _Items( Index ).OnNull( T.Default )
  End Get

  Set ( value As T #1)
    ' -- Contract only applicable to Setter -- 
    Contract
      Clause 1 :  value IsNot Nothing Else value = T.Default
    End Contract
    
    _Items( Index ) = value

  End Set

End Property
C#
default T Item ( Int32 Index #0 )
  /* contract is applicable to both getter and setter */
  contract { [0]{ [ 0 <= Index < ItemCount } else {} }
  get { return _Items[ Index ].OnNull( T.Default ) }
  set( T value #1)
  {
    /* contract is only applicable to setter */
    contract { [1]{ value IsNot Null } else { value = T.Default }
    _Items[ Index ] = value
  }
If a contract clause doesn't have an else clause (or it is empty ) a Breach_Of_Contract_Exception is thrown.

NonNull

With embedded Code Contracts non null-ability could be express as a contract.

The typename postfix operator ! (see: Null Defaults )
 T! x 
Dim x As T!
Is short-hand for the following contract
contract {
          [0]{ T is class }
          [1]{ {x isnot null } else { x = T.Default } }
         }
note Code Contract could a core part of an object definition and variable declaration. So contract enforcement could be tracked.
Aug 14, 2014 at 12:16 PM
Edited Aug 14, 2014 at 12:27 PM
Another possibility is you could also provide contracts.
public static contracts
{
  contract simple_numeric <T>
  {
    [0]{ contracts.comparable<T>   }
    [1]{ contracts.add_operator<T> }
    [2]{ contracts.sub_operator<T> }
    [3]{ contracts.associative<T>  }
    [4]{ contracts.commutative<T>  }
     
  } 
  contract Unit<T> { [0]{ T implements static T Unit() }
  contract      NonNull<T> (T : x) { [0]{ T is class   } 
                                     [1}{ x isnot null } else { x = T.default }
                                   }

  contract   comparable<T> { [0]{ T is IComparable<T> } }
  contract  associative<T> { [0]{ add_operator<T> }
                             [1]{ (x + y) == (y + x) }
  contract add_operator<T> { [0]{ T implements static operator T +(T x, T y) }
  contract sub_operator<T> { [0]{ T implements static operator T -(T x, T y) }
  contract mul_operator<T> { [0]{ T implements static operator T *(T x, T y) }
  contract  commutative<T> { [0]{ contracts.mul_operator<T> }
                             [1]{ (x * y) == (y * x) }
                           }


}
It could then be integrated in to generic constraints
Sub Increment(Of T As { Contracts.Simple_Numeric, Contract.Unit } ) (ByRef x As T )
  x = x + T.Unit
End Sub
Aug 15, 2014 at 6:04 PM
I've update the syntax / grammar to include requires clauses, ensures clause as well as the previous footnotes.
/* C# */
         Digit ::= '0' - '9'
    ElseClause ::= 'else' '{' ContractExpr '}'
        Clause ::= '{' ContractExpr '}' ElseClause? 
      FootNote ::= '[' Digit+ ']' Clause
     FootNotes ::= FootNote+
require_clause ::= '{' Clause '}'
ensures_clause ::= '{' Clause '}'
      requires ::= 'requires' '{' requires_clause* '}'
       ensures ::= 'ensures' '{' ensures_clause* '}'
      contract ::= 'contract' '{' Footnotes? requies? ensures? '}'
contract
{
  [0]{ ... } else { ... }
  [1]{ ... } else { ... }
  requires
  {
    { { ...  } else { ... } }
    { { ...  } else { ... } } 
  }
  ensures
  {
    { { ... } else { ... } }
    { { ... } else { ... } }
  }
}
For the VB.net implementation I'm think along the lines of.

vb stylee
Contract
  Clause 0 : ( ... ) Else ( ... )
  Clause 1 : ( ... ) Else ( ... )
  Requires
     Clause: ( ... ) Else ( ... )
  End Requires
  Ensures
     Clause: ( ,,, ) Else ( ... )
  End Ensures
End Contract
or C#-Esque
Contract
  [0]: ( ... ) Else ( ... )
  [1]: ( ... ) Else ( ... )
  Requires
     ( ... ) Else ( ... )
  End Requires
  Ensures
     ( ... ) Else ( ... )
  End Ensures
End Contract
or Slim-Line
Contract
  [0]: ( ... ) Else ( ... )
  [1]: ( ... ) Else ( ... )
  Requires:
    []: ( ... ) Else ( ... )
    []: ( ... ) Else ( ... )
  Ensures:
    []: ( ... ) Else ( ... )
    []: ( ... ) Else ( ... )
End Contract
Aug 16, 2014 at 2:33 AM
Edited Aug 16, 2014 at 3:28 AM
I think a Code Contract feature would be cool but it looks like your C# samples would be very breaking, considering backwards compatibility.
Having the "Contracts" also assigning default value if the contract has been broken it isn't really a contract anymore, but rather moved logic for assigning default Parameters where i do not see worthy improvement rather than throwing in a if condition at the beginning of the method.
The more interesting part about Code Contracts would be if the compiler and IDE can see at compile-time that you've throw invalid arguments into that method.
I don't think that the scenario "oh i got some crappy parameters, well let's fix it by overriding it with some default" is that common or even a good pattern at all and your sample that replaces null with T.Default could most (all?) of the time be done using optional arguments.
Introducing additional keywords (x isnot null) for expressions that can be expressed in even shorter C# code (x != null) also does not make much sense to me.
Numerating the arguments that are going to be contracted and the amount of curly braces also feels to hurt readability.
Code Contracts were also already somewhat discussed here: https://roslyn.codeplex.com/discussions/560870
And if there is any chance that this Feature would make it into the Language, i would go with the Syntax used by Vala (which took "some" design of C# ;) ): https://wiki.gnome.org/Projects/Vala/Tutorial#Assertions_and_Contract_Programming
Basically it looks mostly like current Code Contracts but it's moved outside the method Body, your first C# example would look like:
object Foo <T>(Int32 Arg1, Int32 Arg2, T Arg0 = default(T)) where T : class
  requires(0 <= Arg1 && Arg1 < XMax)
  requires(0 <= Arg2 && Arg2 < YMax)
{
  /* code body of method */
} 
which looks imho way cleaner, more C#'ish and less new features introducy than
object Foo< T : class > ( T Arg0 #0, Int32 Arg1 #1, Int32 Arg2 #2)
  contract { [0]{ { Arg0 IsNot Null } else { Arg0 = T.Default } }
             [1]{ { [ 0 <= Arg1 < XMax ] } else { } } /* IsBetween ContractExpr */
             [2]{ { [ 0 <= Arg2 < YMax ] } else { } }
           }
{
  /* code body of method */
} 
where
  • you've changed generics to inline constraints
  • changed default(T) to T.Default
  • comparing values against both, a variable and a numeric parameter position, which is very ambiguous
  • introduced a IsNot keyword that is 3 characters longer than !=
And if you look at what stays behind, it's just moving the Contract.Requires into a requires above the method body.
Validating these contracts in real time has already been proven possible on Build 2013 (starting at 00:25:00): http://channel9.msdn.com/Events/Build/2013/3-403
While i desperately hope that they will release that someday, having requires and ensures as language feature would be still interesting though even if it's just translated at compile time into Contract.Requires and Contract.Ensures.
Aug 16, 2014 at 3:17 PM
Edited Aug 16, 2014 at 3:21 PM
Let me yet again state that I not changing Default(T) to T.Default ,
  • T.Default is used to return a non-null instance default for that type (if the type supports non-null ). See
  • Default(T) is the bog standard C# default, if I had use it would have return null (hence no point in having in that contract)
  • Optional Parameter require the optional value to be a Compile-Time constant. Here it doesn't have to be.

... and the amount of curly braces also feels to hurt readability.
It's not by fault that C# is curly brace happy. :-? I'm still experimenting the with the layout and grammar.

You could munge the contract into a single editor line of code.
object Foo< T : class >( T Arg0 , Int32 Arg1 , Int32 Arg2 )
  contract {  requires { Arg0 != null else Arg0 = T.Default ; [ 0 <= Arg1 < XMax ] ;  [ 0 <= Arg2 < YMax ];  }  }
but I think formatting of place each clause on to it own individual editor lines, is easier to read.
object Foo< T : class >( T Arg0 , Int32 Arg1 , Int32 Arg2 )
  contract
  {  requires { Arg0 != null else Arg0 = T.Default ;
                [ 0 <= Arg1 < XMax ] ;
                [ 0 <= Arg2 < YMax ] ;
              }
  }
By having all the explicit braces would allow each individual clause or section to be code-folded.

Footnotes

My premise of footnotes is to have relatively light syntax to express requires clauses, and then have compiler filling the rest.
For example (note: clause is line orientated eol is the end of the clause )
object Foo< T : class >( T Arg0 #0, Int32 Arg1 #1, Int32 Arg2 #2)
  contract { [0]{ != null} else { T.Default }
             [1]{ >= 0   } 
             [1]{ < XMax }
             [2]{ >= 0   }
             [2]{ < YMax }
           }
The clause is only a single statement so the braces could be removed.
object Foo< T : class >( T Arg0 #0, Int32 Arg1 #1, Int32 Arg2 #2)
  contract { [0] != null else  T.Default
             [1] >= 0   
             [1] < XMax 
             [2] >= 0   
             [2] < YMax 
           }
If you specify a footnot on method parameter, but don't supply a corresponding contract clause.
object Foo< T : class >( T Arg0 #0, Int32 Arg1 #1, Int32 Arg2 #2)
The code with not validate the contract and thus fail to compile.

Possible error messages.
1 No footnote contract clause(s) has been provided for parameter ( T arg ) of the method ( Foo<T> )
2 No footnote contract clause(s) has been provided for parameter ( Int32 Arg1 ) of the method ( Foo<T> )
3 No footnote contract clause(s) has been provided for parameter ( Int32 Arg2 ) of the method ( Foo<T> )

Else

Else section of a clause is optional.
If it is not supplied on that particular clause by default it just throws an exception.
else { throw new BreachOfContractException( ) }
The syntax also you to provide an alternative exception.
else { throw new ArgumentException() }
or provide so other value,
else { T.Default }
Would including the return keyword make intent clearer?
else { return T.Default }

else return T.Default

/* both could be valid in the grammar */

Line Orientated Syntax?

Let's examine at using line orientated syntax for contracts.
object Foo< T : class >( T Arg0 #0, Int32 Arg1 #1, Int32 Arg2 #2)
  contract:  [0] != null else  T.Default 
             [1] >= 0    
             [1] < XMax 
             [2] >= 0   
             [2] < YMax 
{
/* rest of code*/
}           
object Foo< T : class >( T Arg0 , Int32 Arg1 , Int32 Arg2 )
  contract: 
     requires: Arg0 != null  else  T.Default 
               [ 0 <= Arg1 < XMax ]
               [ 0 <= Arg2 < YMax ]
{
/* rest of code*/
}             
Conclusion
It has potential of a very clean looking contract code for c#
Aug 16, 2014 at 4:54 PM
AdamSpeight2008 wrote:
Let me yet again state that I not changing Default(T) to T.Default ,
If you would have mentioned in first place that this not existing feature is another draft from you i wouldn't have had to wonder.
  • Optional Parameter require the optional value to be a Compile-Time constant. Here it doesn't have to be.
In that case i would rather argue for dropping that restriction instead of introducing a new syntax for it.
... and the amount of curly braces also feels to hurt readability.
It's not by fault that C# is curly brace happy. :-? I'm still experimenting the with the layout and grammar.
Usually yes but for the previous example, it's exaggerated.
contract { [0]{ {
[1]{ { [
3 curly brackets + 2 brackets,
2 curly backets + 3 brackets
You could munge the contract into a single editor line of code.
object Foo< T : class >( T Arg0 , Int32 Arg1 , Int32 Arg2 )
  contract {  requires { Arg0 != null else Arg0 = T.Default ; [ 0 <= Arg1 < XMax ] ;  [ 0 <= Arg2 < YMax ];  }  }
but I think formatting of place each clause on to it own individual editor lines, is easier to read.
indeed
By having all the explicit braces would allow each individual clause or section to be code-folded.
I don't think that braces are explicit required for that but on the other hand, why would you want to collapse multiple single lines into... single lines with ... ?
The IDE could collapse a contracts block all at once, if you are overwhelmed by contracts your method may have too many arguments.
My premise of footnotes is to have relatively light syntax to express requires clauses, and then have compiler filling the rest.
I'm being a bit skeptical about that shorthand, #n feels to pollute the argumentlist, but without it, it would be harder to read since one could not directly see which contract referrs to which argument. Even with #n it doesn't feels much intuitiv having to lookup contracts with argument position rather than using a meaningful name but that may be just me.
Else
This feels like a hack that could be horrible abused, i would rather go with dropping the constraint on optional arguments (how that one would need to be implemented would be the other question, i'm sure there is a reason why it is required to use a constant value in first place)
Would including the return keyword make intent clearer?
I wonder how Lambdas could be abused for that.
else => T.Default
The argument about custom exceptions could be somewhat addressed like:
object Foo <T>(Int32 Arg1, Int32 Arg2, T Arg0 = default(T)) where T : class
  requires<FooException>(0 <= Arg1 && Arg1 < XMax)
  requires<ArgumentException>(0 <= Arg2 && Arg2 < YMax)
{
  /* code body of method */
}
Aug 16, 2014 at 6:51 PM
Suchiman wrote:
If you would have mentioned in first place that this not existing feature is another draft from you i wouldn't have had to wonder.
I did in the very first post (Non-Null section)


Suchiman wrote:
Usually yes but for the previous example, it's exaggerated.
```
contract { } is defining a contract block, braces are required here.
requires { } is defining a requires clauses block
ensures { } is defining a ensures clauses block
Blocks requires explicit curly braces.

Contract Layout
contract
  footnotes 
  requires
    requires_clause
    requires_clause  
  end requires
  ensures
     ensuires_clause
     ensuires_clause
  end ensures
end contract
Inside the contract block, in doesn't have follow c# grammar rules.
object Foo <T>(Int32 Arg1, Int32 Arg2, T Arg0 = default(T))
  where T : class
  contract { requires {      <FooException> ( ( 0 <= Arg1 ) && ( Arg1 < XMax ) )
                        <ArgumentException> ( ( 0 <= Arg2 ) && ( Arg2 < YMax ) ) } }
{
  /* code body of method */
}
It could follow a different grammar like XML Literals in vb.net.


Suchiman wrote:
I don't think that braces are explicit required for that but on the other hand, why would you want to collapse multiple single lines into... single lines with ... ?
The IDE could collapse a contracts block all at once, if you are overwhelmed by contracts your method may have too many arguments.

It more about allow you collapse, the requires and ensures blocks. As well as the contract block. It'll be a pain in rectum to use regions.
#region "Contract"

#region "Requires"
  

#endregion
#region "Ensure"

#endregion

#endregion

Suchiman wrote:
I'm being a bit skeptical about that shorthand, #n feels to pollute the argumentlist, but without it, it would be harder to read since one could not directly see which contract referrs to which argument. Even with #n it doesn't feels much intuitiv having to lookup contracts with argument position rather than using a meaningful name but that may be just me.
object Foo <T>( Int32 Arg1 #1, Int32 Arg2 #2, T Arg0 = default(T) )
  where T : class
  contract { #1 <FooException>       ( 0 <= _ < XMax )
             #2 <ArgumentException>  ( 0 <= _ < YMax ) }
{
  /* code body of method */
}

I'm think of the error messages. Contract Violation: Clause #1 ( 0 <= _ < XMax )
The Validator / Debugger will supply value of the parameters, like in breakpoints when you highlight a variable.


Suchiman wrote:
The argument about custom exceptions could be somewhat addressed like:
See examples above for alternative. Personally I feel that style for your code contract is a little to wordy for some c# programmers
Aug 16, 2014 at 10:14 PM
AdamSpeight2008 wrote:
Suchiman wrote:
If you would have mentioned in first place that this not existing feature is another draft from you i wouldn't have had to wonder.
I did in the very first post (Non-Null section)
woops sorry, i did even proof read but i totally missed that one.

Taking the failed condition as Exception message sounds good.

AdamSpeight2008 wrote:
Personally I feel that style for your code contract is a little to wordy for some c# programmers
Probably but it's shorter than the current Contract.Requires version, would be interested what other developers think about it.

While we talking about wordiness, the
contract { }
could be omitted i think, it should be uniquely enough that the block starts with requires / ensures before the method body starts.
Aug 16, 2014 at 10:46 PM
Suchiman wrote:
While we talking about wordiness, the
contract { }
could be omitted i think, it should be uniquely enough that the block starts with requires / ensures before the method body starts.
You probably could but I think good to have some indication what the code block is. VB.net has the Block ... End Block structure.

vb.net
Function Foo(Of T : Class)( Arg1 As Int32 #1, Arg2 As Integer #2, Optional Arg0 As T = Nothing) As Object
  Contract
    #1 <FooException>      ( 0 <= _ < XMax )
    #2 <ArgumentException> ( 0 <= _ < YMax ) 
  End Contract
  ' -- code body of method --
End Function


Function Foo(Of T : Class)( Arg1 As Int32, Arg2 As Integer, Optional Arg0 As T = Nothing) As Object
  Contract
    Requires
      <FooException>      ( 0 <= _ < XMax )
      <ArgumentException> ( 0 <= _ < YMax )       
    End Requires
    Ensures
      ( Foo IsNot Nothing ) 
    End Ensures
  End Contract
  ' -- code body of method --
End Function
Aug 25, 2014 at 12:43 PM
Edited Aug 25, 2014 at 12:48 PM
Extending the Object base class, could lead to some interest possibilities.
class Object 
{
  abstract bool Equals(Object other)
  abstract Int32 GetHashcode()
  abstract String ToString()
  abstract IContract Contract() get: set:      /* Each object can have its own contract. */
  static abstract Object! DefaultTo()  /* Non-Null default */
}
The contract can be manipulated at runtime, made readonly.
var int x {requires: 0 <= x < 99 } = 0;
var string s {requires: s != nulll) }= "";

class WeirdList < T : { requires: T != WeirdList } >
{
}

class Point ( int x {requires: x >= 0} , int y {requires: y >= 0 } )
  contract: {Ensures: Point <: Immutable; Point <: NonNull }

struct Point ( int x, int y )
  contract: { Ensures: Point <: Immutable } /* enforce immutability */