Design by Contract (DbC) design considerations

1

Here is my thinking on the DbC feature ...

Implement the full semantics of Eiffel DbC and improve upon it.

Don’t use annotations - Ughhh. Many contract frameworks tack it on and the expressions are all enclosed in a string which prevents syntax highlighting, refactoring, type checking etc DdC needs to be built into the language itself and so IDEA can work with it in the AST.

Don’t forget “check” assertions - they are also useful in addition to require, ensure and invariant.

I was thinking along the lines of :

{code}

require
  there must be at least one product :                  products.size > 0

  the product index must be within the valid range :    index > 0 && index <= products.length,

                                                           “The index {index} is not within the range 0 to {products.length}”

{code}

(This is very close to how I implemented a simple DbC framework in groovy many years ago)

This is not exactly following Eiffel, I have made the following improvements:

  1. Mandatory labels
      These are important as its good to have a human readable version of the assertion because:
      a) It aids the USER of a framework in understanding how to use it.
      b) It helps diagnose bugs when the label is added to a contract violaton exception then logged or alerted to the developer.

  2. Contract violation messages
      Added into the exception, these give more details about the offending values to help track bugs faster.

  3. Ordering is significant
      The second requirement is dependent on the first. i.e. if the first is violated the second is not relevent. This saves duplicating the first assertion in the second just to avoid multiple violations.

  4. Allow some variable initialisation code prior to requirement assertion in a method.

On the topic of multiple violations perhaps there is an opportunity here to allow multiple violations and define the dependencies e.g.:

{code}
init
  val languages = allProducts.filter {it.category == language}
  val MAX_PRICE = 1000

require
  there must be at least one language product :           languages.size > 0
           {
           the product index must be within the valid range :   index > 0 && index <= products.length,
                                                                  “The index {index} is not within the range 0 to {products.length}”

           all languages must be cheap:                          languages.forall {it.price < MAX_PRICE},
                                                                  “These languages are not cheap: {languages.filter {it.price >= MAX_PRICE}}”
           }

{code}

In the case above the last two requirements could both be violated giving the developer more information up front.
This means adding more than one contract violation to a single exception - perhaps this is too complex.

2

FWIW the current standard library has a require function which behaves close to your example though using the current language syntax; so it can be used anywhere a statement can be: 

fun foo() {
  require( products.size > 0, "there must be at least one product " )
  ...
  require( index > 0 && index <= products.length, "The index {index} is not within the range 0 to {products.length}" )
}

though we've no custom language syntax to use these expressions outside of a function body though

3

Yes, this is the way I implemented basic DbC like assertions in Groovy 5 years ago. In that framework the exceptions were much more than an alias for assert. It added info about what kind of assertion it was require/ensure/check and fiddled with the stack trace to get the right source line of the contract assertion.

I was never happy with it because I wanted more: invariants, inheritance of contracts, the old keyword for ensures etc - just like eiffel.
Since then GContracts has done more than I but it still lacks labels and messages. We can borrow some of the GContracts work and do better with Kotlin.

4

Would be so nice to have class invariants evaluated at beginning and end of methods…