Assertion (software development): Difference between revisions

Content deleted Content added
m Ok
Tags: Visual edit Mobile edit Mobile web edit
Changing short description from "In computer programming, statement that a predicate is always true at that point in code execution" to "Statement that a predicate is always true at that point in code execution"
 
(35 intermediate revisions by 27 users not shown)
Line 1:
{{Short description|Statement that a predicate is always true at that point in code execution}}
{{About|the computer programming concept ok|assertions in the context of the [[Security Assertion Markup Language]] (SAML) open standard|Security Assertion Markup Language#Assertions}}
 
In [[computer programming]], specifically when using the [[imperative programming]] paradigm, an '''assertion''' is a [[Predicate (mathematical logic)|predicate]] (a [[Boolean-valued function]] over the [[state space]], usually expressed as a [[logical proposition]] using the [[variable (programming)|variable]]s of a program) connected to a point in the program, that always should evaluate to true at that point in code execution. Assertions can help a programmer read the code, help a [[compiler]] compile it, or help the program detect its own defects.
 
For the latter, some programs check assertions by actually evaluating the predicate as they run. Then, if it is not in fact true – an assertion failure –, the program considers itself to be broken and typically deliberately [[Crash (computing)|crashes]] or throws an assertion failure [[exception handling|exception]].
 
== Details ==
 
The following code contains two assertions, <code>x > 0</code> and <code>x > 1</code>, and they are indeed true at the indicated points during execution:
<sourcesyntaxhighlight lang="cjava">
x = 1;
assert x > 0;
x++;
assert x > 1;
</syntaxhighlight>
</source>
 
Programmers can use assertions to help specify programs and to reason about program correctness. For example, a [[precondition]]—an assertion placed at the beginning of a section of code—determines the set of states under which the programmer expects the code to execute. A [[postcondition]]—placed at the end—describes the expected state at the end of execution. For example: <code>x > 0 { x++ } x > 1</code>.
 
The example above uses the notation for including assertions used by [[C. A. R. Hoare]] in his 1969 article.<ref>[[C. A. R. Hoare]], [http://lambda-the-ultimate.org/node/1912 An axiomatic basis for computer programming], ''[[Communications of the ACM]]'', 1969.</ref> That notation cannot be used in existing mainstream programming languages. However, programmers can include unchecked assertions using the [[Comment (computer programming)|comment feature]] of their programming language. For example, in [[C (programming language)|C++]]:
 
<sourcesyntaxhighlight lang="Cc">
x = 5;
x = x + 1;
// {x > 1}
</syntaxhighlight>
</source>
 
The braces included in the comment help distinguish this use of a comment from other uses.
 
[[Library (computing)|Libraries]] may provide assertion features as well. For example, in C using [[glibc]] with C99 support:
 
<sourcesyntaxhighlight lang="Cc">
#include <assert.h>
 
Line 38 ⟶ 39:
assert(x > 1);
}
</syntaxhighlight>
</source>
 
Several modern programming languages include checked assertions – [[statement (programming)|statements]] that are checked at [[Run time (program lifecycle phase)|runtime]] or sometimes statically. If an assertion evaluates to false at runtime, an assertion failure results, which typically causes execution to abort. This draws attention to the ___location at which the logical inconsistency is detected and can be preferable to the behaviour that would otherwise result.
Line 46 ⟶ 47:
== Usage ==
 
In languages such as [[Eiffel (programming language)|Eiffel]], assertions form part of the design process; other languages, such as [[C (programming language)|C]] and [[Java (programming language)|Java]], use them only to check assumptions at [[Runtime system|runtime]]. In both cases, they can be checked for validity at runtime but can usually also be suppressed.
 
=== Assertions in design by contract ===
Line 58 ⟶ 59:
An assertion may be used to verify that an assumption made by the programmer during the implementation of the program remains valid when the program is executed. For example, consider the following [[Java (programming language)|Java]] code:
 
<sourcesyntaxhighlight lang="java">
int total = countNumberOfUsers();
if (total % 2 == 0) {
// total is even
} else {
// total is odd and non-negative
assert total % 2 == 1;
}
</syntaxhighlight>
</source>
 
In [[Java (programming language)|Java]], <code>%</code> is the ''[[remainder]]'' operator (''[[Modulo operation|modulo]]''), and in Java, if its first operand is negative, the result can also be negative (unlike the modulo used in mathematics). Here, the programmer has assumed that <code>total</code> is non-negative, so that the remainder of a division with 2 will always be 0 or 1. The assertion makes this assumption explicit: if <code>countNumberOfUsers</code> does return a negative value, the program may have a bug.
Line 95 ⟶ 96:
Static assertions are particularly useful in compile time [[template metaprogramming]], but can also be used in low-level languages like C by introducing illegal code if (and only if) the assertion fails. [[C1X|C11]] and [[C++11]] support static assertions directly through <code>static_assert</code>. In earlier C versions, a static assertion can be implemented, for example, like this:
 
<sourcesyntaxhighlight lang="c">
#define SASSERT(pred) switch(0){case 0:case pred:;}
 
SASSERT( BOOLEAN CONDITION );
</syntaxhighlight>
</source>
 
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:
 
<sourcesyntaxhighlight lang="c">
static char const static_assertion[ (BOOLEAN CONDITION)
? 1 : -1
] = {'!'};
</syntaxhighlight>
</source>
 
If the <code>(BOOLEAN CONDITION)</code> part evaluates to false then the above code will not compile because arrays may not have a negative length. If in fact the compiler allows a negative length then the initialization byte (the <code>'!'</code> part) should cause even such over-lenient compilers to complain. 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.
 
Both of these methods require a method of constructing unique names. Modern compilers support a <code>__COUNTER__</code> preprocessor define that facilitates the construction of unique names, by returning monotonically increasing numbers for each compilation unit.<ref>[https://gcc.gnu.org/gcc-4.3/changes.html GNU, "GCC 4.3 Release Series&nbsp;— Changes, New Features, and Fixes"]</ref>
 
[[D (programming language)|D]] provides static assertions through the use of <code>static assert</code>.<ref>Static{{cite assertionsweb in| url = D''http://dlang.org/version.html#StaticAssert'' | work = D Language Reference | title = Static Assertions | publisher = The D Language Foundation | accessdate = 2022-03-16}}</ref>
 
== Disabling assertions ==
Line 121 ⟶ 122:
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 effects]]) 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]], [[ZPE_Programming_Environment|YASS]] and [[C++]], can 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.
 
Similarly, launching the [[Python (programming language)|Python]] interpreter with "{{Mono|-O}}" (for "optimize") as an argument will cause the Python code generator to not emit any bytecode for asserts.<ref>[https://docs.python.org/3/reference/simple_stmts.html#grammar-token-assert-stmt Official Python Docs, ''assert statement'']</ref>
 
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 [[Just-in-time compilation|JIT compiler]] at run-time or [[dead_code_elimination|excluded at compile time]] via the programmer manually placing each assertion behind an <code>if (false)</code> clause.
 
Programmers can build checks into their code that are always active by bypassing or manipulating the language's normal assertion-checking mechanisms.
Line 127 ⟶ 132:
== Comparison with error handling ==
 
Assertions are distinct from routine [[Exception handling|error-handling]]. Assertions document logically impossible situations and discover programming errors: if the impossible occurs, then something fundamental is clearly wrong with the program. This is distinct from error handling: most error conditions are possible, although some may be extremely unlikely to occur in practice. Using assertions as a general-purpose error handling mechanism is unwise: assertions do not allow for recovery from errors; an assertion failure will normally halt the program's execution abruptly; and assertions are often disabled in production code. Assertions also do not display a user-friendly error message.
 
Consider the following example of using an assertion to handle an error:
 
<sourcesyntaxhighlight lang="c">
int *ptr = malloc(sizeof(int) * 10);
assert(ptr);
// use ptr
...
</syntaxhighlight>
</source>
 
Here, the programmer is aware that <code>[[malloc]]</code> will return a [[Null pointer|<code>NULL</code> pointer]] if memory is not allocated. This is possible: the operating system does not guarantee that every call to <code>malloc</code> will succeed. If an out of memory error occurs the program will immediately abort. Without the assertion, the program would continue running until <code>ptr </code> was dereferenced, and possibly longer, depending on the specific hardware being used. So long as assertions are not disabled, an immediate exit is assured. But if a graceful failure is desired, the program has to handle the failure. For example, a server may have multiple clients, or may hold resources that will not be released cleanly, or it may have uncommitted changes to write to a datastore. In such cases it is better to fail a single transaction than to abort abruptly.
 
Another error is to rely on side effects of expressions used as arguments of an assertion. One should always keep in mind that assertions might not be executed at all, since their sole purpose is to verify that a condition which should always be true does in fact hold true. Consequently, if the program is considered to be error-free and released, assertions may be disabled and will no longer be evaluated.
Line 144 ⟶ 149:
Consider another version of the previous example:
 
<sourcesyntaxhighlight lang="c">
int *ptr;
// Statement below fails if malloc() returns NULL,
// but is not executed at all when compiling with -NDEBUG!
assert(ptr = malloc(sizeof(int) * 10));
// use ptr: ptr isn't initialised when compiling with -NDEBUG!
...
</syntaxhighlight>
</source>
 
This might look like a smart way to assign the return value of <code>malloc</code> to <code>ptr</code> and check if it is <code>NULL</code> in one step, but the <code>malloc</code> call and the assignment to <code>ptr</code> is a side effect of evaluating the expression that forms the <code>assert</code> condition. When the <code>NDEBUG</code> parameter is passed to the compiler, as when the program is considered to be error-free and released, the <code>assert()</code> statement is removed, so <code>malloc()</code> isn't called, rendering <code>ptr</code> uninitialised. This could potentially result in a [[segmentation fault]] or similar [[null pointer]] error much further down the line in program execution, causing bugs that may be [[Heisenbug|sporadic]] and/or difficult to track down. Programmers sometimes use a similar VERIFY(X) define to alleviate this problem.
 
Modern compilers may issue a warning when encountering the above code.<ref>{{Cite web|url=https://gcc.gnu.org/onlinedocs/gcc/Warning-Options.html#index-Wparentheses-367|title=Warning Options (Using the GNU Compiler Collection (GCC))}}</ref>
 
== 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"] {{Webarchive|url=https://web.archive.org/web/20181112230722/https://library.ias.edu/files/pdfs/ecp/planningcodingof0103inst.pdf |date=2018-11-12 }}. 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. [httphttps://www.turingarchive.orgkings.cam.ac.uk/viewerpublications-lectures-and-talks-amtb/?id=462&title=01amt-b-8 Checking a Large Routine], 1949; quoted in C. A. R. Hoare, "The Emperor's Old Clothes", 1980 Turing Award lecture.</ref>
 
== See also ==
Line 177 ⟶ 182:
== External links ==
 
* ''[http://www.oracle.com/us/technologies/java/assertions-139853.html Programming With Assertions in Java]'' by Qusay H. Mahmoud, (Oracle Corp.), 2005
* ''[http://discovery.ucl.ac.uk/4991/1/4991.pdf A historical perspective on runtime assertion checking in software development]'' by Lori A. Clarke, David S. Rosenblum in: ACM SIGSOFT Software Engineering Notes 31(3):25-37, 2006
* ''[httphttps://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=1203056 Assertions: a personal perspective]'' by C.A.R. Hoare in: IEEE Annals of the History of Computing, Volume: 25, Issue: 2 (2003), Page(s): 14 - 2514–25
* ''[http://www.pgbovine.net/programming-with-asserts.htm The benefits of programming with assertions]'' by Philip Guo (Stanford University), 2008
* ''[http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=1203056 Assertions: a personal perspective]'' by C.A.R. Hoare in: IEEE Annals of the History of Computing, Volume: 25, Issue: 2 (2003), Page(s): 14 - 25
* ''[http://queue.acm.org/detail.cfm?id=2220317 My Compiler Does Not Understand Me]'' by Poul-Henning Kamp in: ACM Queue 10(5), May 2012
* ''[https://blog.regehr.org/archives/1091 Use of Assertions]'' by John Regehr