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

Library: Scala

The last line is only executed if all assertions are met.<lang scala>import java.net.{URLDecoder, URLEncoder}

import scala.compat.Platform.currentTime

object UrlCoded extends App {

 val original = """http://foo bar/"""
 val encoded: String = URLEncoder.encode(original, "UTF-8")

 assert(encoded == "http%3A%2F%2Ffoo+bar%2F", s"Original: $original not properly encoded: $encoded")

 val percentEncoding = encoded.replace("+", "%20")
 assert(percentEncoding == "http%3A%2F%2Ffoo%20bar%2F", s"Original: $original not properly percent-encoded: $percentEncoding")

 assert(URLDecoder.decode(encoded, "UTF-8") == URLDecoder.decode(percentEncoding, "UTF-8"))

 println(s"Successfully completed without errors. [total ${currentTime - executionStart} ms]")

}</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