Assertion (software development): Difference between revisions

Revision as of 09:35, 15 October 2017

Revision as of 23:21, 29 October 2017

Line 48:

=== Assertions in design by contract ===

Assertions can function as a form of documentation: they can describe the state the code expects to find before it runs (its [[precondition]]s), and the state the code expects to result in when it is finished running ([[postcondition]]s); they can also specify [[invariant (computer science)|invariantinvariants]]s of a [[Class (computer science)|class]]. [[Eiffel (programming language)|Eiffel]] integrates such assertions into the language and automatically extracts them to document the class. This forms an important part of the method of [[design by contract]].

This approach is also useful in languages that do not explicitly support it: the advantage of using assertion statements rather than assertions in [[comment (computer programming)|commentcomments]]s is that the program can check the assertions every time it runs; if the assertion no longer holds, an error can be reported. This prevents the code from getting out of sync with the assertions.

=== Assertions for run-time checking ===

Line 101:

If the <code>(BOOLEAN CONDITION)</code> part evaluates to false then the above code will not compile because the compiler will not allow two [[Switch statement#C and languages with C-like syntax|case labels]] with the same constant. The boolean expression must be a compile-time constant value, for example <code>(sizeof(int)==4)</code> would be a valid expression in that context. This construct does not work at file scope (i.e. not inside a function), and so it must be wrapped inside a function.

Another popular <ref>Jon Jagger, ''[http://www.jaggersoft.com/pubs/CVu11_3.html Compile Time Assertions in C]'', 1999.</ref> way of implementing assertions in C is:

<source lang="c">

Line 117:

== Disabling assertions ==

Most languages allow assertions to be enabled or disabled globally, and sometimes independently. Assertions are often enabled during development and disabled during final testing and on release to the customer. Not checking assertions avoids the cost of evaluating the assertions while (assuming the assertions are free of [[Side-effect (computer science)|side effecteffects]]s) still producing the same result under normal conditions. Under abnormal conditions, disabling assertion checking can mean that a program that would have aborted will continue to run. This is sometimes preferable.

Some languages, including [[C (programming language)|C]] and [[C++]], completely remove assertions at compile time using the [[preprocessor]]. Java requires an option to be passed to the run-time engine in order to enable assertions. Absent the option, assertions are bypassed, but they always remain in the code unless optimised away by a JIT compiler at run-time or excluded by an if(false) condition at compile time, thus they need not have a run-time space or time cost in Java either.

Line 156:

== History ==

In 1947 reports by [[John von Neumann|von Neumann]] and [[Herman Goldstine|Goldstine]]<ref>Goldstine and von Neumann. [https://library.ias.edu/files/pdfs/ecp/planningcodingof0103inst.pdf"Planning and Coding of problems for an Electronic Computing Instrument"]. Part II, Volume I, 1 April 1947, p.  12.</ref> on their design for the [[IAS machine]], they described algorithms using an early version of [[Flowchart|flow charts]], in which they included assertions: "It may be true, that whenever C actually reaches a certain point in the flow diagram, one or more bound variables will necessarily possess certain specified values, or possess certain properties, or satisfy certain properties with each other. Furthermore, we may, at such a point, indicate the validity of these limitations. For this reason we will denote each area in which the validity of such limitations is being asserted, by a special box, which we call an assertion box."

The assertional method for proving correctness of programs was advocated by [[Alan Turing]]. In a talk "Checking a Large Routine" at Cambridge, June 24, 1949 Turing suggested: "How can one check a large routine in the sense of making sure that it's right? In order that the man who checks may not have too difficult a task, the programmer should make a number of definite ''assertions'' which can be checked individually, and from which the correctness of the whole program easily follows".<ref>Alan Turing. [http://www.turingarchive.org/viewer/?id=462&title=01 Checking a Large Routine], 1949; quoted in C.  A.  R. Hoare, "The Emperor's Old Clothes", 1980 Turing Award lecture.</ref>

== See also ==