Anonymous user
Assertions: Difference between revisions
Added SPARK version.
(Added SPARK version.) |
|||
Line 483:
raises an <tt>AssertionFailed</tt> condition (an <tt>Error</tt>).
=={{header|SPARK}}==
Works with SPARK GPL 2010
Assertions are analysed statically, before compilation or execution. They can appear in various places:
:inline in the code, either
<lang ada>-# check X = 42;</lang>
::or
<lang ada>-# assert X = 42;</lang>
:as a precondition on an operation:
<lang ada>procedure P (X : in out Integer);
--# derives X from *;
--# pre X = 42;</lang>
:or as a postcondition on an operation:
<lang ada>procedure P (X : in out Integer);
--# derives X from *;
--# post X = 42;</lang>
Example:
<lang ada>X := 7;
--# check X = 42;</lang>
produces the following output:
<pre>H1: true .
->
C1: false .</pre>
which is an unprovable theorem that tells you that there is a guaranteed failure.
=={{header|Tcl}}==
{{libheader|tcllib}}
| |||