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.

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