Assertions in design by contract

Assertions in design by contract is a draft programming task. It is not yet considered ready to be promoted as a complete task, for reasons that should be found in its talk page.

According to Wikipedia; Assertions can function as a form of documentation: they can describe the state the code expects to find before it runs (its preconditions), and the state the code expects to result in when it is finished running (postconditions); they can also specify invariants of a class.

Show in the program language of your choice an example of the expecting results as a form of documentation.

Go

The Go FAQ states:

Why does Go not have assertions?

Go doesn't provide assertions. They are undeniably convenient, but our experience has been that programmers use them as a crutch to avoid thinking about proper error handling and reporting. Proper error handling means that servers continue operation after non-fatal errors instead of crashing. Proper error reporting means that errors are direct and to the point, saving the programmer from interpreting a large crash trace. Precise errors are particularly important when the programmer seeing the errors is not familiar with the code.

We understand that this is a point of contention. There are many things in the Go language and libraries that differ from modern practices, simply because we feel it's sometimes worth trying a different approach.

The "contract" in "design by contract" should be embodied in the API and error return values (if any) not in assertions that are typically only compiled when debugging.

If someone disagrees and they really want to use an "assert" they can simply roll their own: <lang go>func assert(t bool, s string) { if !t { panic(s) } } //… assert(c == 0, "some text here") </lang> (And if the assert function was defined in a file with build constraints and a stub in a file with the opposite constraint then they could be effectively be enabled/disabled at compile time. That's probably a bad idea.)

Scala

Scala provides runtime assertions like Java: they are designed to be used by static analysis tools however the default compiler doesn’t perform such analyses by default. The Scala assertions (assume, require, assert, ensuring) are Predef library methods that are enabled by default and can be disabled using the -Xdisable-assertions runtime flag, unlike Java where assertions are disabled by default and enabled with a runtime flag. It is considered poor form to rely on assertions to validate arguments, because they can be disabled. An appropriate informative runtime exception (e.g. NullPointerException or IllegalArgumentException) should be thrown instead. <lang Scala>object AssertionsInDesignByContract extends App {

   /**
    * @param ints a non-empty array of integers
    * @return the mean magnitude of the array's elements.
    */
   def averageOfMagnitudes(ints: Array[Int]) = {
       // assertions for static analysis / runtime protoyping:
       assume(ints != null, "array must not be null")
       require(ints.length > 0, "array must be non-empty")
       // runtime exceptions when assertions are disabled:
       if (ints.length < 1) throw new IllegalArgumentException("Cannot find the average of an empty array")
       // note, the above line can implicitly throw a NullPointerException too
       val abs = ints.map(Math.abs)
       val mean = Math.round(abs.sum.toDouble / ints.length)
       assert(Math.abs(mean) >= abs.min && Math.abs(mean) <= abs.max, "magnitude must be within range")
       mean
   } ensuring(_ >= 0, "result must be non-negative (possible overflow)")

   println(averageOfMagnitudes(Array(1))) // 1
   println(averageOfMagnitudes(Array(1,3))) // 2
   println(averageOfMagnitudes(null)) // java.lang.AssertionError: assumption failed: array must not be null
   println(averageOfMagnitudes(Array(Integer.MAX_VALUE, Integer.MAX_VALUE))) // java.lang.AssertionError: assertion failed: magnitude must be within range
   println(averageOfMagnitudes(Array(Integer.MAX_VALUE, 1))) // java.lang.AssertionError: assertion failed: result must be non-negative (possible overflow)

}</lang>

Tcl

<lang tcl># Custom assertions; names stolen from Eiffel keywords proc require {expression message args} {

   if {![uplevel 1 [list expr $expression]]} {

set msg [uplevel 1 [list format $message] $args] return -level 2 -code error "PRECONDITION FAILED: $msg"

   }

} proc ensure {expression {message ""} args} {

   if {![uplevel 1 [list expr $expression]]} {

set msg [uplevel 1 [list format $message] $args] return -level 2 -code error "POSTCONDITION FAILED: $msg"

   }

}

proc connect_to_server {server port} {

   require {$server ne ""} "server address must not be empty"
   require {[string is integer -strict $port]} "port must be numeric"
   require {$port > 0 && $port < 65536} "port must be valid for client"

   set sock [socket $server $port]

   # Will never fail: Tcl *actually* throws an error on connection
   # failure instead, but the principle still holds.
   ensure {$sock ne ""} "a socket should have been created"

   return $sock

}</lang> This can be usefully mixed with Tcl 8.6's try … finally … built-in command.

Example output from above code:

% connect_to_server "" ""
PRECONDITION FAILED: server address must not be empty
% connect_to_server localhost 123456
PRECONDITION FAILED: port must be valid for client