Assertions in design by contract: Difference between revisions

From Rosetta Code
Content added Content deleted
(corrected spelling)
m (→‎{{header|Wren}}: Minor tidy)
 
(23 intermediate revisions by 8 users not shown)
Line 7: Line 7:
Show in the program language of your choice an example of the use of assertions as a form of documentation.
Show in the program language of your choice an example of the use of assertions as a form of documentation.
<br><br>
<br><br>

=={{header|6502 Assembly}}==
The <code>BRK</code> opcode can be used to trap errors. It causes a jump to the IRQ vector, but it skips one extra byte upon returning. That byte can be used to hold your error code.

The hard part is telling the difference between a <code>BRK</code> and a normal interrupt request. While the 6502 technically has a break flag, the way you read it is different from the way you would typically read the flags.

You '''cannot''' read the break flag this way:
<syntaxhighlight lang="6502asm">php ;NV-BDIZC (N=negative V=overflow B=break D=decimal I=Interrupt Z=Zero C=Carry)
pla
and #%00010000
BNE BreakSet</syntaxhighlight>

This is because the processor flags register doesn't actually contain the true status of the break flag. The only way to read the break flag is to read the flags value that was pushed onto the stack by the hardware itself. Fortunately, this is always at the top of the stack just after an interrupt. Unfortunately, we can't read the flags without clobbering at least one of our registers, something we can't afford to do during an interrupt of any kind. So we'll need to account for the registers we're pushing onto the stack when searching for the flags.

<syntaxhighlight lang="6502asm">tempPC_Lo equ $20 ;an arbitrary zero page address set aside for debugging
tempPC_Hi equ $21 ;this must be one byte higher than the previous address.

foo:
LDA #$7F
CLC
ADC #$01
BVC continue
BRK
byte $02 ;put your desired error code here
continue:
;rest of program

IRQ:
PHA
TXA
PHA
TYA
PHA ;push all.
TSX ;loads the stack pointer into X.
LDA $0104,X ;read the break flag. Normally this would be at offset $0101,X, but since we pushed the three registers we had to add 3.
AND #$10
BNE debug ;if the break flag is set, you got here because of a BRK command.
;else, this was a normal IRQ.


;rest of program

debug:
;we need the pushed PC, minus 1.
LDA $0105,X ;get the low program counter byte
SEC
SBC #1
STA tempPC_Lo
LDA $0106,X
SBC #0
STA tempPC_Hi
LDY #0
LDA (tempPC),y ;get the error code that was stored immediately after the BRK
;now do whatever you want with that info, such as display a relevant error message to the screen etc.


;rest of program

org $FFFA
dw NMI,RESET,IRQ</syntaxhighlight>

=={{header|68000 Assembly}}==
Error handlers are referred to as <i>traps</i> on the 68000, and they can be triggered automatically (such as attempting to divide by zero) and by command (such as for if overflow has occurred.)

Precondition example:
<syntaxhighlight lang="68000devpac"> DIVU D3,D2 ;this will cause a jump to the "divide by zero trap" if D3 = 0.</syntaxhighlight>

Postcondition examples:
<syntaxhighlight lang="68000devpac"> ADD.L D4,D5
TRAPV ;no overflow is expected, so if it occurs call the relevant trap.</syntaxhighlight>

<syntaxhighlight lang="68000devpac"> LSL.W #8,D2 ;shift D2 left 8 bits.
bcc continue ;if carry clear, we're good.
trap 9 ;otherwise call trap 9, which has been defined (in this example only) to handle unexpected carries after a bit shift.

continue: ;the program resumes normally after this point</syntaxhighlight>


=={{header|Ada}}==
=={{header|Ada}}==
Ada 2012 introduced aspect specifications to the language. Aspect specifications may be used to specify characteristics about data types, procedures, functions, and tasks. Frequently used aspect specifications for procedures and functions include the ability to specify preconditions and post-conditions. Aspect specifications are written as part of a procedure or function specification such as:
Ada 2012 introduced aspect specifications to the language. Aspect specifications may be used to specify characteristics about data types, procedures, functions, and tasks. Frequently used aspect specifications for procedures and functions include the ability to specify preconditions and post-conditions. Aspect specifications are written as part of a procedure or function specification such as:
<lang Ada>type Nums_Array is array (Integer range <>) of Integer;
<syntaxhighlight lang="ada">type Nums_Array is array (Integer range <>) of Integer;


procedure Sort(Arr : in out Nums_Array) with
procedure Sort(Arr : in out Nums_Array) with
Pre => Arr'Length > 1,
Pre => Arr'Length > 1,
Post => (for all I in Arr'First .. Arr'Last -1 => Arr(I) <= Arr(I + 1));
Post => (for all I in Arr'First .. Arr'Last -1 => Arr(I) <= Arr(I + 1));
</syntaxhighlight>
</lang>
The precondition above requires the array to be sorted to have more than one data element.
The precondition above requires the array to be sorted to have more than one data element.


Line 21: Line 97:


Post conditions can also reference parameter changes made during the operation of the procedure such as the following procedure specifications for an unbounded queue:
Post conditions can also reference parameter changes made during the operation of the procedure such as the following procedure specifications for an unbounded queue:
<lang Ada> procedure Enqueue (Item : in out Queue; Value : Element_Type) with
<syntaxhighlight lang="ada"> procedure Enqueue (Item : in out Queue; Value : Element_Type) with
Post => Item.Size = Item'Old.Size + 1;
Post => Item.Size = Item'Old.Size + 1;
procedure Dequeue (Item : in out Queue; Value : out Element_Type) with
procedure Dequeue (Item : in out Queue; Value : out Element_Type) with
Pre => not Item.Is_Empty,
Pre => not Item.Is_Empty,
Post => Item.Size = Item'Old.Size - 1;
Post => Item.Size = Item'Old.Size - 1;
</syntaxhighlight>
</lang>
Since this is an unbounded queue there is no size constraint on the Enqueue procedure. The Dequeue procedure can only function properly if the queue is not empty.
Since this is an unbounded queue there is no size constraint on the Enqueue procedure. The Dequeue procedure can only function properly if the queue is not empty.


Line 32: Line 108:


Type invariants can be specified using aspect clauses such as:
Type invariants can be specified using aspect clauses such as:
<lang Ada>subtype Evens is Integer range 0..Integer'Last with
<syntaxhighlight lang="ada">subtype Evens is Integer range 0..Integer'Last with
Dynamic_Predicate => Evens mod 2 = 0;
Dynamic_Predicate => Evens mod 2 = 0;


type Data is array (Natural range <>) of Integer;
type Data is array (Natural range <>) of Integer;
subtype Limits is Data with
subtype Limits is Data with
Dynamic_Predicate => (for all I in Data'First..Data'Last - 1 => Data(I) < Data(I + 1));
Dynamic_Predicate => (for all I in Limits'First..Limits'Last - 1 => Limits(I) < Limits(I + 1));


type Days is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
type Days is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
subtype Alternates is Days with
subtype Alternates is Days with
Static_Predicate => Alternates in Mon | Wed | Fri | Sun;
Static_Predicate => Alternates in Mon | Wed | Fri | Sun;
</syntaxhighlight>
</lang>
The Dynamic_Predicate used for subtype Evens above specifies that each value of the subtype must be an even number.
The Dynamic_Predicate used for subtype Evens above specifies that each value of the subtype must be an even number.


Line 52: Line 128:
{{trans|D}}
{{trans|D}}
Algol W has assertions. Although pre and post conditions are not built in to the language, assertions can be used to simulate them.
Algol W has assertions. Although pre and post conditions are not built in to the language, assertions can be used to simulate them.
<lang algolw>begin
<syntaxhighlight lang="algolw">begin
long real procedure averageOfAbsolutes( integer array values( * )
long real procedure averageOfAbsolutes( integer array values( * )
; integer value valuesLength
; integer value valuesLength
Line 72: Line 148:
write( averageOfAbsolutes( v, 2 ) )
write( averageOfAbsolutes( v, 2 ) )
end
end
end.</lang>
end.</syntaxhighlight>
{{out}}
{{out}}
<pre>
<pre>
Line 80: Line 156:
=={{header|D}}==
=={{header|D}}==
D has exceptions, errors and asserts. In Phobos there is also an enforce(). D has pre-conditions and post conditions, and struct/class invariants. Class method contracts should work correctly in object oriented code with inheritance.
D has exceptions, errors and asserts. In Phobos there is also an enforce(). D has pre-conditions and post conditions, and struct/class invariants. Class method contracts should work correctly in object oriented code with inheritance.
<lang d>import std.stdio, std.algorithm, std.math;
<syntaxhighlight lang="d">import std.stdio, std.algorithm, std.math;


double averageOfAbsolutes(in int[] values) pure nothrow @safe @nogc
double averageOfAbsolutes(in int[] values) pure nothrow @safe @nogc
Line 106: Line 182:
Foo f;
Foo f;
f.inc;
f.inc;
}</lang>
}</syntaxhighlight>
{{out}}
{{out}}
<pre>2</pre>
<pre>2</pre>
Line 112: Line 188:
=={{header|Eiffel}}==
=={{header|Eiffel}}==
{{trans|D}}
{{trans|D}}
<lang eiffel> acc: INTEGER
<syntaxhighlight lang="eiffel"> acc: INTEGER
average_of_absolutes (values: ARRAY[INTEGER]): INTEGER
average_of_absolutes (values: ARRAY[INTEGER]): INTEGER
require
require
Line 122: Line 198:
ensure
ensure
non_neg_result: Result >= 0
non_neg_result: Result >= 0
end</lang>
end</syntaxhighlight>


=={{header|Fortran}}==
=={{header|Fortran}}==
Fortran offers no formal "assert" protocol, but there would be nothing to stop a programmer devising a subroutine such as <lang Fortran> SUBROUTINE AFFIRM(CONDITION,MESSAGE)
Fortran offers no formal "assert" protocol, but there would be nothing to stop a programmer devising a subroutine such as <syntaxhighlight lang="fortran"> SUBROUTINE AFFIRM(CONDITION,MESSAGE)
LOGICAL CONDITION
LOGICAL CONDITION
CHARACTER*(*) MESSAGE
CHARACTER*(*) MESSAGE
Line 131: Line 207:
WRITE (6,*) MESSAGE
WRITE (6,*) MESSAGE
STOP "Oops. Confusion!"
STOP "Oops. Confusion!"
END </lang>
END </syntaxhighlight>
And then scattering through the source file lines such as <lang Fortran> CALL AFFIRM(SSQ.GE.0,"Sum of squares can't be negative.") !Perhaps two passes should be used.</lang>
And then scattering through the source file lines such as <syntaxhighlight lang="fortran"> CALL AFFIRM(SSQ.GE.0,"Sum of squares can't be negative.") !Perhaps two passes should be used.</syntaxhighlight>
And this could be combined with the arrangements described in [[Stack_traces#Fortran]] to provide further interesting information.
And this could be combined with the arrangements described in [[Stack_traces#Fortran]] to provide further interesting information.


As written, the scheme involves an unconditional invocation of a subroutine with parameters. That overhead would be reduced by something like <lang Fortran> IF (SSQ.LT.0) CALL CROAK("Sum of squares can't be negative.") !Perhaps two passes should be used.</lang>
As written, the scheme involves an unconditional invocation of a subroutine with parameters. That overhead would be reduced by something like <syntaxhighlight lang="fortran"> IF (SSQ.LT.0) CALL CROAK("Sum of squares can't be negative.") !Perhaps two passes should be used.</syntaxhighlight>


Some compilers allowed a D in column one to signify that this was a debugging statement, and a compiler option could specify that all such statements were to be treated as comments and not compiled. Probably not a good idea for statements performing checks. The code that is run with intent to produce results should be the same code that you have tested... A variation on this theme involves such debugging output being written to a file, then after modifying and recompiling, the new version's execution proceeds only while it produces the same debugging output. The reference output could be considered a (voluminous) contract, but for this to work a special testing environment is required and is not at all a Fortran standard.
Some compilers allowed a D in column one to signify that this was a debugging statement, and a compiler option could specify that all such statements were to be treated as comments and not compiled. Probably not a good idea for statements performing checks. The code that is run with intent to produce results should be the same code that you have tested... A variation on this theme involves such debugging output being written to a file, then after modifying and recompiling, the new version's execution proceeds only while it produces the same debugging output. The reference output could be considered a (voluminous) contract, but for this to work a special testing environment is required and is not at all a Fortran standard.
Line 142: Line 218:


FreeBASIC provides three assertions. The <code>#assert</code> preprocessor directive will cause compilation to halt with an error message if its argument evaluates to zero:
FreeBASIC provides three assertions. The <code>#assert</code> preprocessor directive will cause compilation to halt with an error message if its argument evaluates to zero:
<lang freebasic>#assert SCREENX >= 320</lang>
<syntaxhighlight lang="freebasic">#assert SCREENX >= 320</syntaxhighlight>


The macro <code>assert</code> will halt at runtime with an error message if its argument evaluates to zero:
The macro <code>assert</code> will halt at runtime with an error message if its argument evaluates to zero:
<lang freebasic>'compile with the -g flag
<syntaxhighlight lang="freebasic">'compile with the -g flag
assert( Pi < 3 )</lang>
assert( Pi < 3 )</syntaxhighlight>


Finally, <code>assertwarn</code> is like <code>assert</code> but only prints an error message and continues running:
Finally, <code>assertwarn</code> is like <code>assert</code> but only prints an error message and continues running:
<lang freebasic>'compile with the -g flag
<syntaxhighlight lang="freebasic">'compile with the -g flag
dim as integer a = 2
dim as integer a = 2
assertwarn( a+a=5 )
assertwarn( a+a=5 )
print "Ha, no."</lang>
print "Ha, no."</syntaxhighlight>


All three show the line number of the failed assertion and the expression that failed, making these nicely self-documenting.
All three show the line number of the failed assertion and the expression that failed, making these nicely self-documenting.
Line 171: Line 247:


If someone disagrees and they ''really'' want to use an "assert" they can simply roll their own:
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) {
<syntaxhighlight lang="go">func assert(t bool, s string) {
if !t {
if !t {
panic(s)
panic(s)
Line 178: Line 254:
//…
//…
assert(c == 0, "some text here")
assert(c == 0, "some text here")
</syntaxhighlight>
</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.)
(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.)


Line 184: Line 260:
J can load scripts expecting any non-assigned noun result to be all 1's.
J can load scripts expecting any non-assigned noun result to be all 1's.
If the file tautology_script.ijs contains
If the file tautology_script.ijs contains
<syntaxhighlight lang="j">
<lang J>
NB. demonstrate properties of arithmetic
NB. demonstrate properties of arithmetic
'A B C' =: 3 ?@$ 0 NB. A B and C are random floating point numbers in range [0, 1).
'A B C' =: 3 ?@$ 0 NB. A B and C are random floating point numbers in range [0, 1).
Line 191: Line 267:
(A * B) -: (B * A) NB. scalar multiplication commutes
(A * B) -: (B * A) NB. scalar multiplication commutes
(A * (B + C)) -: ((A * B) + (A * C)) NB. distributive property
(A * (B + C)) -: ((A * B) + (A * C)) NB. distributive property
</syntaxhighlight>
</lang>
we could load it into a session as 0!:3<'tautology_script.ijs' with result of 1, because the expressions match (-:). Were a sentence to fail the result would be 0, as for example replacing multiplication with matrix product and A B and C with square matrices of same size.
we could load it into a session as 0!:3<'tautology_script.ijs' with result of 1, because the expressions match (-:). Were a sentence to fail the result would be 0, as for example replacing multiplication with matrix product and A B and C with square matrices of same size.


In next example the assertion both tests substitute when the script loads and shows how to use substitute. Infinity (_) replaces the zeros in the y argument, and the x argument is the vector zero infinity.
In next example the assertion both tests substitute when the script loads and shows how to use substitute. Infinity (_) replaces the zeros in the y argument, and the x argument is the vector zero infinity.
<syntaxhighlight lang="j">
<lang J>
substitute =: 4 : '[&.((y~:{.x)&(#!.({:x)))y'
substitute =: 4 : '[&.((y~:{.x)&(#!.({:x)))y'
assert _ 1 1 _ 2 -: 0 _ substitute 0 1 1 0 2
assert _ 1 1 _ 2 -: 0 _ substitute 0 1 1 0 2
</lang>
</syntaxhighlight>




Pre-condition adverbs with example:
Pre-condition adverbs with example:
<syntaxhighlight lang="j">
<lang J>
Positive =: adverb define
Positive =: adverb define
'non-positive' assert *./ , y > 0
'non-positive' assert *./ , y > 0
Line 223: Line 299:
|non-positive: assert
|non-positive: assert
| 'non-positive' assert*./,y>0
| 'non-positive' assert*./,y>0
</syntaxhighlight>
</lang>


As a post-condition, and this is contrived because a better definition of exact_factorial would be !@:x: ,
As a post-condition, and this is contrived because a better definition of exact_factorial would be !@:x: ,
<syntaxhighlight lang="j">
<lang J>
IntegralResult =: adverb define
IntegralResult =: adverb define
RESULT =. u y
RESULT =. u y
Line 248: Line 324:
|use extended precision!: assert
|use extended precision!: assert
| 'use extended precision!' assert(<datatype RESULT)e.;:'extended integer'
| 'use extended precision!' assert(<datatype RESULT)e.;:'extended integer'
</syntaxhighlight>
</lang>


One could assert an invariant in quicksort such that following the split the maximum of the small group is less than the minimum of the large group:
One could assert an invariant in quicksort such that following the split the maximum of the small group is less than the minimum of the large group:
Line 256: Line 332:
The ''-ea'' or ''-enableassertions'' option must be passed to the VM when running the application for this to work.<br>
The ''-ea'' or ''-enableassertions'' option must be passed to the VM when running the application for this to work.<br>
Example taken from [[Perceptron#Java|Perceptron task]].
Example taken from [[Perceptron#Java|Perceptron task]].
<lang java>(...)
<syntaxhighlight lang="java">(...)
int feedForward(double[] inputs) {
int feedForward(double[] inputs) {
assert inputs.length == weights.length : "weights and input length mismatch";
assert inputs.length == weights.length : "weights and input length mismatch";
Line 266: Line 342:
return activate(sum);
return activate(sum);
}
}
(...)</lang>
(...)</syntaxhighlight>

=={{header|jq}}==
{{libheader|Jq/assert.jq}}
{{works with|jq}}

jq does not currently support assertions natively though they (and
design by contract) can be simulated as here, using a jq module.

The [https://gist.github.com/pkoppstein/9b0f49a213a5b8083bab094ede06652d "assert.jq"] module
allows assertion checking to be turned on or off; in addition,
execution can be continued or terminated after an assertion violation is detected.

In the following, it is assumed the "debug" mode of assertion checking has been used, e.g.
via the invocation: jq --arg assert debug

This mode allows execution to continue after an assertion violation has been detected.
<syntaxhighlight lang="jq">
include "rc-assert" {search: "."}; # or use the -L command-line option

def averageOfAbsolutes:
. as $values
# pre-condition
| assert(type == "array" and length > 0 and all(type=="number");
"input to averageOfAbsolutes should be a non-empty array of numbers.")
| (map(length) | add/length) as $result
# post-condition
| assert($result >= 0;
$__loc__ + { msg: "Average of absolute values should be non-negative."} )
| $result;

[1, 3], ["hello"]
| averageOfAbsolutes
</syntaxhighlight>
{{output}}
Invocation: jq -n --arg assert debug -f assertions.jq
<pre>
2
["DEBUG:","assertion violation @ input to averageOfAbsolutes should be a non-empty array of numbers. => false"]
5
</pre>


=={{header|Julia}}==
=={{header|Julia}}==
The @assert macro is used for assertions in Julia.
The @assert macro is used for assertions in Julia.
<lang julia>function volumesphere(r)
<syntaxhighlight lang="julia">function volumesphere(r)
@assert(r > 0, "Sphere radius must be positive")
@assert(r > 0, "Sphere radius must be positive")
return π * r^3 * 4.0 / 3.0
return π * r^3 * 4.0 / 3.0
end
end
</syntaxhighlight>
</lang>


=={{header|Kotlin}}==
=={{header|Kotlin}}==
<lang scala>// version 1.1.2
<syntaxhighlight lang="scala">// version 1.1.2
// requires -ea JVM option
// requires -ea JVM option


Line 284: Line 400:
println("The following command line arguments have been passed:")
println("The following command line arguments have been passed:")
for (arg in args) println(arg)
for (arg in args) println(arg)
}</lang>
}</syntaxhighlight>


{{out}}
{{out}}
Line 297: Line 413:
2
2
</pre>
</pre>

=={{header|Nim}}==
Nim provides two kind of assertions: assertions which can be deactivated by compiling without checks and assertions which cannot be deactivated.

The first kind takes the form: <code>assert boolean_expression</code> with a default message or <code>assert boolean_expression, message</code> when with want a specific message.
For the second kind, <code>assert</code> is simply replaced with <code>doAssert</code>.

Assertions may be used anywhere, either as preconditions, post-conditions or invariants.

Here is an example:

<syntaxhighlight lang="nim">import math

func isqrt(n: int): int =
assert n >= 0, "argument of “isqrt” cannot be negative"
int(sqrt(n.toFloat))</syntaxhighlight>

If the assertion is not true, the program terminates in error with the exception AssertionDefect:
<pre>Error: unhandled exception: test.nim(2, 10) `n >= 0` argument of “isqrt” cannot be negative [AssertionDefect]</pre>

Note also that, in this case, rather than using an assertion, we could have simply specified that “n” must be a natural:

<syntaxhighlight lang="nim">import math

func isqrt(n: Natural): int =
int(sqrt(n.toFloat))</syntaxhighlight>

If the argument is negative, we get the following error:
<pre>Error: unhandled exception: value out of range: -1 notin 0 .. 9223372036854775807 [RangeDefect]</pre>


=={{header|Perl}}==
=={{header|Perl}}==
{{trans|Raku}}
{{trans|Raku}}
<lang Perl># 20201201 added Perl programming solution
<syntaxhighlight lang="perl"># 20201201 added Perl programming solution


use strict;
use strict;
Line 326: Line 471:
MessageMultiplier->new(2,'A')->execute;
MessageMultiplier->new(2,'A')->execute;
dies_ok { MessageMultiplier->new(1,'B')->execute };
dies_ok { MessageMultiplier->new(1,'B')->execute };
dies_ok { MessageMultiplier->new(3, '')->execute };</lang>
dies_ok { MessageMultiplier->new(3, '')->execute };</syntaxhighlight>
{{out}}
{{out}}
<pre>1..2
<pre>1..2
Line 335: Line 480:
=={{header|Phix}}==
=={{header|Phix}}==
User defined types can be used to directly implement design by contract, and disabled by "without type_check".
User defined types can be used to directly implement design by contract, and disabled by "without type_check".
<!--<syntaxhighlight lang="phix">-->
<lang Phix>type hour(object x)
<span style="color: #008080;">type</span> <span style="color: #000000;">hour</span><span style="color: #0000FF;">(</span><span style="color: #004080;">object</span> <span style="color: #000000;">x</span><span style="color: #0000FF;">)</span>
return integer(x) and x>=0 and x<=23
<span style="color: #008080;">return</span> <span style="color: #004080;">integer</span><span style="color: #0000FF;">(</span><span style="color: #000000;">x</span><span style="color: #0000FF;">)</span> <span style="color: #008080;">and</span> <span style="color: #000000;">x</span><span style="color: #0000FF;">>=</span><span style="color: #000000;">0</span> <span style="color: #008080;">and</span> <span style="color: #000000;">x</span><span style="color: #0000FF;"><=</span><span style="color: #000000;">23</span>
end type
<span style="color: #008080;">end</span> <span style="color: #008080;">type</span>
hour h
<span style="color: #000000;">hour</span> <span style="color: #000000;">h</span>
h = 1 -- fine
<span style="color: #000000;">h</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">1</span> <span style="color: #000080;font-style:italic;">-- fine</span>
h = 26 -- bad</lang>
<span style="color: #000000;">h</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">26</span> <span style="color: #000080;font-style:italic;">-- bad (desktop/Phix only)</span>
<!--</syntaxhighlight>-->
{{out}}
{{out}}
<pre>
<pre>
Line 349: Line 496:


You can also (since 0.8.2) use standard assert statemnents, eg
You can also (since 0.8.2) use standard assert statemnents, eg
<!--<syntaxhighlight lang="phix">(phixonline)-->
<lang Phix>assert(fn!=-1,"cannot open config file")</lang>
<span style="color: #004080;">integer</span> <span style="color: #000000;">fn</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">-1</span> <span style="color: #000080;font-style:italic;">-- (try also 1)</span>
<span style="color: #7060A8;">assert</span><span style="color: #0000FF;">(</span><span style="color: #000000;">fn</span><span style="color: #0000FF;">!=-</span><span style="color: #000000;">1</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"cannot open config file"</span><span style="color: #0000FF;">)</span>
<!--</syntaxhighlight>-->


=={{header|Racket}}==
=={{header|Racket}}==
Line 366: Line 516:
This example is extremely surface-scratching.
This example is extremely surface-scratching.


<lang racket>
<syntaxhighlight lang="racket">
#lang racket
#lang racket
(require racket/contract)
(require racket/contract)
Line 421: Line 571:
;; the bad function doesn't have a chance to generate an invalid reply
;; the bad function doesn't have a chance to generate an invalid reply
(show-contract-failure (average-of-absolutes:bad 42))
(show-contract-failure (average-of-absolutes:bad 42))
(show-contract-failure (average-of-absolutes:bad '())))</lang>
(show-contract-failure (average-of-absolutes:bad '())))</syntaxhighlight>


{{out}}
{{out}}
Line 501: Line 651:


In this snippet, the routine repeat takes one Integer that must be greater than 1, a String and returns a String. (Note that as written, it is incorrect since it actually returns a boolean.)
In this snippet, the routine repeat takes one Integer that must be greater than 1, a String and returns a String. (Note that as written, it is incorrect since it actually returns a boolean.)
<lang perl6>sub repeat ( Int $repeat where * > 1, Str $message, --> Str ) {
<syntaxhighlight lang="raku" line>sub repeat ( Int $repeat where * > 1, Str $message, --> Str ) {
say $message x $repeat;
say $message x $repeat;
True # wrong return type
True # wrong return type
Line 521: Line 671:
.resume;
.resume;
}
}
}</lang>
}</syntaxhighlight>
{{out}}
{{out}}
<pre>AA
<pre>AA
Line 535: Line 685:


=={{header|REXX}}==
=={{header|REXX}}==
This is just a simple method of ''assertion''; &nbsp; more informative messages could be added in the &nbsp; '''assertion''' &nbsp; routine.
This is just a simple method of &nbsp; ''assertion''; &nbsp; more informative messages could be added in the &nbsp; '''assertion''' &nbsp; routine.
<br>A &nbsp; '''return''' &nbsp; statement could've been used instead of an &nbsp; '''exit''' &nbsp; statement to continue processing.
<br>A &nbsp; '''return''' &nbsp; statement could've been used instead of an &nbsp; '''exit''' &nbsp; statement to continue processing.
<lang rexx>/*REXX program demonstrates a method on how to use assertions in design by contract.*/
<syntaxhighlight lang="rexx">/*REXX program demonstrates a method on how to use assertions in design by contract.*/
parse arg top . /*obtain optional argument from the CL.*/
parse arg top . /*obtain optional argument from the CL.*/
if top=='' | top=="," then top=100 /*Not specified? Then use the default.*/
if top=='' | top=="," then top= 100 /*Not specified? Then use the default.*/
pad=left('', 9) /*PAD contains nine blanks for SAYs. */
_= left('', 9) /*_: contains 9 blanks for SAY passing*/
w= length(top) + 1 /*W: is used for aligning the output. */

do #=1 for 666 /*repeat for a devilish number of times*/
do #=1 for 666 /*repeat for a devilish number of times*/
a=random(1, top) /*generate a random number (1 ──► TOP)*/
a= random(1, top) /*generate a random number (1 ──► TOP)*/
b=random(1, a) /* " " " " (1 ──► A)*/
b= random(1, a) /* " " " " (1 ──► A)*/
c=a-b /*compute difference between A and B. */
c= a - b /*compute difference between A and B. */
say pad 'a=' right(a,4) pad "b=" right(b,4) pad 'c=' right(c,4)
say _'a='right(a, w)_"b="right(b, w)_'c='right(c, w)_"sum="right(sumABC(a, b, c), w)
call assert date('Weekday')\=="Monday" /*shouldn't execute this pgm on Monday.*/
call assert date('Weekday') \== "Monday" /*shouldn't execute this pgm on Monday.*/
call assert time('H')<9 | time("H")>15 /* ··· and not during banking hours.*/
call assert time('H')<9 | time("H")>15 /* ··· and not during banking hours.*/
call assert c>0 /*The value of C must be positive. */
call assert c>0 /*The value of C must be positive. */
sum=my_sub(a, b, c) /*invoke a subroutine to do "stuff". */
say copies(' ',60) 'sum=' sum /*display the sum of A, B, and C. */
end /*#*/
end /*#*/
exit /*stick a fork in it, we're all done. */
exit 0 /*stick a fork in it, we're all done. */
/*──────────────────────────────────────────────────────────────────────────────────────*/
/*──────────────────────────────────────────────────────────────────────────────────────*/
assert: if arg(1) then return 1; say /*if true, then assertion has passed. */
assert: if arg(1) then return 1; say /*if true, then assertion has passed. */
say 'assertion failed on line ' sigL " with: " subword(space(sourceline(sigl)),3)
say 'assertion failed on line ' sigL " with: " subword(space(sourceline(sigl)),2)
say; say '# index= ' #
say; say '# index= ' #
say 'ASSERT is exiting.'; exit 13
say 'ASSERT is exiting.'; exit 13
/*──────────────────────────────────────────────────────────────────────────────────────*/
/*──────────────────────────────────────────────────────────────────────────────────────*/
my_sub: return arg(1) +arg(2) +arg(3) /*Sum three arguments. Real easy work.*/</lang>
sumABC: procedure; parse arg x,y,z; return x+y+z /*Sum three arguments. Real easy work.*/</syntaxhighlight>
'''output''' &nbsp; when using the default input:
{{out|output|text=&nbsp; when using the default input:}}
<pre>
<pre>
a= 6 b= 5 c= 1
a= 12 b= 5 c= 7 sum= 24
sum= 12
a= 88 b= 77 c= 11 sum= 176
a= 88 b= 17 c= 71
a= 35 b= 26 c= 9 sum= 70
sum= 176
a= 33 b= 9 c= 24 sum= 66
a= 34 b= 12 c= 22
a= 90 b= 31 c= 59 sum= 180
sum= 68
a= 64 b= 9 c= 55 sum= 128
a= 100 b= 97 c= 3
a= 82 b= 18 c= 64 sum= 164
sum= 200
a= 6 b= 4 c= 2 sum= 12
a= 88 b= 52 c= 36
a= 85 b= 72 c= 13 sum= 170
sum= 176
a= 74 b= 49 c= 25 sum= 148
a= 17 b= 9 c= 8
a= 31 b= 14 c= 17 sum= 62
sum= 34
a= 58 b= 48 c= 10 sum= 116
a= 29 b= 11 c= 18
a= 64 b= 59 c= 5 sum= 128
sum= 58
a= 53 b= 1 c= 52 sum= 106
a= 23 b= 1 c= 22
a= 54 b= 22 c= 32 sum= 108
sum= 46
a= 36 b= 9 c= 27 sum= 72
a= 100 b= 35 c= 65
a= 2 b= 2 c= 0 sum= 4
sum= 200
a= 10 b= 8 c= 2
sum= 20
a= 1 b= 1 c= 0


assertion failed on line 13 with: c>0 /*The value of C must be positive. */
assertion failed on line 13 with: assert c>0 /*The value of C must be positive. */


# index= 11
# index= 17
ASSERT is exiting.
ASSERT is exiting.
</pre>
</pre>


=={{header|Ruby}}==
=={{header|Ruby}}==
<lang ruby>
<syntaxhighlight lang="ruby">
require 'contracts'
require 'contracts'
include Contracts
include Contracts
Line 602: Line 746:


puts double("oops")
puts double("oops")
</syntaxhighlight>
</lang>
{{out}}
{{out}}
<pre>
<pre>
Line 615: Line 759:
=={{header|Scala}}==
=={{header|Scala}}==
Scala provides runtime assertions like Java: they are designed to be used by static analysis tools however the default compiler doesn’t perform such analyses by default. The Scala assertions (<tt>assume</tt>, <tt>require</tt>, <tt>assert</tt>, <tt>ensuring</tt>) are [http://www.scala-lang.org/api/current/index.html#scala.Predef$ Predef library] methods that are enabled by default and can be disabled using the <tt>-Xdisable-assertions</tt> runtime flag, unlike Java where assertions are disabled by default and enabled with a runtime flag. It is considered poor form to rely on assertions to validate arguments, because they can be disabled. An appropriate informative runtime exception (e.g. NullPointerException or IllegalArgumentException) should be thrown instead.
Scala provides runtime assertions like Java: they are designed to be used by static analysis tools however the default compiler doesn’t perform such analyses by default. The Scala assertions (<tt>assume</tt>, <tt>require</tt>, <tt>assert</tt>, <tt>ensuring</tt>) are [http://www.scala-lang.org/api/current/index.html#scala.Predef$ Predef library] methods that are enabled by default and can be disabled using the <tt>-Xdisable-assertions</tt> runtime flag, unlike Java where assertions are disabled by default and enabled with a runtime flag. It is considered poor form to rely on assertions to validate arguments, because they can be disabled. An appropriate informative runtime exception (e.g. NullPointerException or IllegalArgumentException) should be thrown instead.
<lang Scala>object AssertionsInDesignByContract extends App {
<syntaxhighlight lang="scala">object AssertionsInDesignByContract extends App {
/**
/**
* @param ints a non-empty array of integers
* @param ints a non-empty array of integers
Line 639: Line 783:
println(averageOfMagnitudes(Array(Integer.MAX_VALUE, Integer.MAX_VALUE))) // java.lang.AssertionError: assertion failed: magnitude must be within range
println(averageOfMagnitudes(Array(Integer.MAX_VALUE, Integer.MAX_VALUE))) // java.lang.AssertionError: assertion failed: magnitude must be within range
println(averageOfMagnitudes(Array(Integer.MAX_VALUE, 1))) // java.lang.AssertionError: assertion failed: result must be non-negative (possible overflow)
println(averageOfMagnitudes(Array(Integer.MAX_VALUE, 1))) // java.lang.AssertionError: assertion failed: result must be non-negative (possible overflow)
}</lang>
}</syntaxhighlight>


=={{header|Tcl}}==
=={{header|Tcl}}==
<lang tcl># Custom assertions; names stolen from Eiffel keywords
<syntaxhighlight lang="tcl"># Custom assertions; names stolen from Eiffel keywords
proc require {expression message args} {
proc require {expression message args} {
if {![uplevel 1 [list expr $expression]]} {
if {![uplevel 1 [list expr $expression]]} {
Line 668: Line 812:


return $sock
return $sock
}</lang>
}</syntaxhighlight>
This can be usefully mixed with Tcl 8.6's <code>try … finally …</code> built-in command.
This can be usefully mixed with Tcl 8.6's <code>try … finally …</code> built-in command.


Line 678: Line 822:
PRECONDITION FAILED: port must be valid for client
PRECONDITION FAILED: port must be valid for client
</pre>
</pre>

=={{header|Wren}}==
{{trans|D}}
{{libheader|Wren-assert}}
Wren doesn't support assertions natively though they (and design by contract) can be simulated using a library.
<syntaxhighlight lang="wren">import "./assert" for Assert
import "./math" for Nums

// Assert.disabled = true

var averageOfAbsolutes = Fn.new { |values|
// pre-condition
Assert.ok(values.count > 0, "Values list must be non-empty.")

var result = Nums.mean(values.map { |v| v.abs })
// post-condition
Assert.ok(result >= 0, "Average of absolute values should be non-negative.")
return result
}

class Foo {
construct new(x) {
_x = x
checkInvariant_()
}

x { _x }
x=(v) {
_x = v
checkInvariant_()
}

inc {
// no need to check invariance here
_x = _x + 1
}

checkInvariant_() {
Assert.ok(_x >= 0, "Field 'x' must be non-negative.")
}
}

System.print(averageOfAbsolutes.call([1, 3]))
var f = Foo.new(-1)
f.inc
System.print(f.x)</syntaxhighlight>

{{out}}
With assertions enabled:
<pre>
2
Field 'x' must be non-negative.
[./assert line 225] in fail(_)
[./assert line 71] in ok(_,_)
[./assertions_in_DBC line 34] in checkInvariant_()
[./assertions_in_DBC line 19] in init new(_)
[./assertions_in_DBC line 20] in
[./assertions_in_DBC line 39] in (script)
</pre>
or with assertions disabled (un-comment line 4):
<pre>
2
0
</pre>

=={{header|Z80 Assembly}}==
There are no built-in assertions, error handlers, etc. at the hardware level. The closest you can get is a function conditionally returning early. For example, this function for multiplication checks if the second factor equals zero or 1 before attempting to multiply.
<syntaxhighlight lang="z80">SmallMultiply:
;returns A = C * A
or a ;compares A to zero
ret z ;returns with the product A = C * 0 = 0.
dec a ;sets zero flag if A equaled 1 prior to decrement, effectively comparing A to 1.
jr z, C_Times_One
ld b,a
ld a,c
loop_smallMultiply:
add c
djnz loop_smallMultiply
ret ;returns A = C * A


C_Times_One:
ld a,c
ret ;returns A = C</syntaxhighlight>


=={{header|zkl}}==
=={{header|zkl}}==
zkl has exceptions. The _assert_ keyword just wraps the AssertionError exception. _assert_ takes an expression and optional message.
zkl has exceptions. The _assert_ keyword just wraps the AssertionError exception. _assert_ takes an expression and optional message.
There are no pre/post conditionals.
There are no pre/post conditionals.
<lang zkl>fcn f(a){
<syntaxhighlight lang="zkl">fcn f(a){
_assert_((z:=g())==5,"I wanted 5, got "+z)
_assert_((z:=g())==5,"I wanted 5, got "+z)
}</lang>
}</syntaxhighlight>
Running the code throws an exception with file and line number:
Running the code throws an exception with file and line number:
{{out}}
{{out}}

Latest revision as of 09:41, 7 November 2023

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.


Task

Show in the program language of your choice an example of the use of assertions as a form of documentation.

6502 Assembly

The BRK opcode can be used to trap errors. It causes a jump to the IRQ vector, but it skips one extra byte upon returning. That byte can be used to hold your error code.

The hard part is telling the difference between a BRK and a normal interrupt request. While the 6502 technically has a break flag, the way you read it is different from the way you would typically read the flags.

You cannot read the break flag this way:

php  ;NV-BDIZC (N=negative V=overflow B=break D=decimal I=Interrupt Z=Zero C=Carry)
pla
and #%00010000
BNE BreakSet

This is because the processor flags register doesn't actually contain the true status of the break flag. The only way to read the break flag is to read the flags value that was pushed onto the stack by the hardware itself. Fortunately, this is always at the top of the stack just after an interrupt. Unfortunately, we can't read the flags without clobbering at least one of our registers, something we can't afford to do during an interrupt of any kind. So we'll need to account for the registers we're pushing onto the stack when searching for the flags.

tempPC_Lo equ $20 ;an arbitrary zero page address set aside for debugging
tempPC_Hi equ $21 ;this must be one byte higher than the previous address.

foo:
LDA #$7F
CLC
ADC #$01
BVC continue
BRK
byte $02  ;put your desired error code here
continue:
;rest of program

IRQ:
PHA
TXA
PHA
TYA
PHA          ;push all. 
TSX          ;loads the stack pointer into X.
LDA $0104,X  ;read the break flag. Normally this would be at offset $0101,X, but since we pushed the three registers we had to add 3.
AND #$10
BNE debug    ;if the break flag is set, you got here because of a BRK command.
;else, this was a normal IRQ.


;rest of program

debug:
;we need the pushed PC, minus 1.
LDA $0105,X  ;get the low program counter byte
SEC
SBC #1
STA tempPC_Lo
LDA $0106,X
SBC #0
STA tempPC_Hi
LDY #0
LDA (tempPC),y  ;get the error code that was stored immediately after the BRK
;now do whatever you want with that info, such as display a relevant error message to the screen etc.


;rest of program

org $FFFA
dw NMI,RESET,IRQ

68000 Assembly

Error handlers are referred to as traps on the 68000, and they can be triggered automatically (such as attempting to divide by zero) and by command (such as for if overflow has occurred.)

Precondition example:

    DIVU D3,D2  ;this will cause a jump to the "divide by zero trap" if D3 = 0.

Postcondition examples:

    ADD.L D4,D5
    TRAPV    ;no overflow is expected, so if it occurs call the relevant trap.
    LSL.W #8,D2  ;shift D2 left 8 bits. 
    bcc continue ;if carry clear, we're good.
        trap 9   ;otherwise call trap 9, which has been defined (in this example only) to handle unexpected carries after a bit shift.

continue:        ;the program resumes normally after this point

Ada

Ada 2012 introduced aspect specifications to the language. Aspect specifications may be used to specify characteristics about data types, procedures, functions, and tasks. Frequently used aspect specifications for procedures and functions include the ability to specify preconditions and post-conditions. Aspect specifications are written as part of a procedure or function specification such as:

type Nums_Array is array (Integer range <>) of Integer;

procedure Sort(Arr : in out Nums_Array) with
    Pre => Arr'Length > 1,
    Post => (for all I in Arr'First .. Arr'Last -1 => Arr(I) <= Arr(I + 1));

The precondition above requires the array to be sorted to have more than one data element.

The post condition describes the state of the array after being sorted, stating that the array must consist of only increasing values or duplicate values.

Post conditions can also reference parameter changes made during the operation of the procedure such as the following procedure specifications for an unbounded queue:

   procedure Enqueue (Item : in out Queue; Value : Element_Type) with
      Post => Item.Size = Item'Old.Size + 1;
   procedure Dequeue (Item : in out Queue; Value : out Element_Type) with
      Pre  => not Item.Is_Empty,
      Post => Item.Size = Item'Old.Size - 1;

Since this is an unbounded queue there is no size constraint on the Enqueue procedure. The Dequeue procedure can only function properly if the queue is not empty.

The post-condition for Enqueue simply states that the size of the queue after enqueuing an element is one more than the size of the queue before enqueuing the element. Similarly the post-condition for Dequeue states that after the dequeuing an element the size of the queue is one less than the size of the queue before dequeuing the element.

Type invariants can be specified using aspect clauses such as:

subtype Evens is Integer range 0..Integer'Last with
    Dynamic_Predicate => Evens mod 2 = 0;

type Data is array (Natural range <>) of Integer;
subtype Limits is Data with
    Dynamic_Predicate => (for all I in Limits'First..Limits'Last - 1 => Limits(I) < Limits(I + 1));

type Days is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
subtype Alternates is Days with
    Static_Predicate => Alternates in Mon | Wed | Fri | Sun;

The Dynamic_Predicate used for subtype Evens above specifies that each value of the subtype must be an even number.

The Dynamic_Predicate used for subtype Limits specifies that the array must contain data in increasing value with no duplicates.

The Static_Predicate used for subtype Alternates specifies a type which is a discontinuous subtype of Days.

ALGOL W

Translation of: D

Algol W has assertions. Although pre and post conditions are not built in to the language, assertions can be used to simulate them.

begin
    long real procedure averageOfAbsolutes( integer array values( * )
                                          ; integer value valuesLength
                                          ) ;
    begin
        long real av;
        % Pre-condition. %
        assert( valuesLength > 0 );
        for i := 1 until valuesLength do av := av + abs( values( i ) );
        av := av / valuesLength;
        % Post-condition. %
        assert( av >= 0 );
        av
    end averageOfAbsolutes ;
    begin
        integer array v( 1 :: 2 );
        v( 1 ) := 1; v( 2 ) := 3;
        r_format := "A"; r_w := 6; r_d := 2; % set output formatting %
        write( averageOfAbsolutes( v, 2 ) )
    end
end.
Output:
  2.00

D

D has exceptions, errors and asserts. In Phobos there is also an enforce(). D has pre-conditions and post conditions, and struct/class invariants. Class method contracts should work correctly in object oriented code with inheritance.

import std.stdio, std.algorithm, std.math;

double averageOfAbsolutes(in int[] values) pure nothrow @safe @nogc
in {
    // Pre-condition.
    assert(values.length > 0);
} out(result) {
    // Post-condition.
    assert(result >= 0);
} body {
    return values.map!abs.sum / double(values.length);
}

struct Foo {
    int x;
    void inc() { x++; }
    invariant {
        // Struct invariant.
        assert(x >= 0);
    }
}

void main() {
    [1, 3].averageOfAbsolutes.writeln;
    Foo f;
    f.inc;
}
Output:
2

Eiffel

Translation of: D
  acc: INTEGER
  average_of_absolutes (values: ARRAY[INTEGER]): INTEGER
    require
      non_empty_values: values.count > 0
    do
      acc := 0
      values.do_all(agent abs_sum)
      Result := acc // values.count
    ensure
      non_neg_result: Result >= 0
    end

Fortran

Fortran offers no formal "assert" protocol, but there would be nothing to stop a programmer devising a subroutine such as

      SUBROUTINE AFFIRM(CONDITION,MESSAGE)
        LOGICAL CONDITION
        CHARACTER*(*) MESSAGE
         IF (CONDITION) RETURN      !All is well.
         WRITE (6,*) MESSAGE
         STOP "Oops. Confusion!"
       END

And then scattering through the source file lines such as

      CALL AFFIRM(SSQ.GE.0,"Sum of squares can't be negative.")   !Perhaps two passes should be used.

And this could be combined with the arrangements described in Stack_traces#Fortran to provide further interesting information.

As written, the scheme involves an unconditional invocation of a subroutine with parameters. That overhead would be reduced by something like

      IF (SSQ.LT.0) CALL CROAK("Sum of squares can't be negative.")   !Perhaps two passes should be used.

Some compilers allowed a D in column one to signify that this was a debugging statement, and a compiler option could specify that all such statements were to be treated as comments and not compiled. Probably not a good idea for statements performing checks. The code that is run with intent to produce results should be the same code that you have tested... A variation on this theme involves such debugging output being written to a file, then after modifying and recompiling, the new version's execution proceeds only while it produces the same debugging output. The reference output could be considered a (voluminous) contract, but for this to work a special testing environment is required and is not at all a Fortran standard.

FreeBASIC

FreeBASIC provides three assertions. The #assert preprocessor directive will cause compilation to halt with an error message if its argument evaluates to zero:

#assert SCREENX >= 320

The macro assert will halt at runtime with an error message if its argument evaluates to zero:

'compile with the -g flag
assert( Pi < 3 )

Finally, assertwarn is like assert but only prints an error message and continues running:

'compile with the -g flag
dim as integer a = 2
assertwarn( a+a=5 )
print "Ha, no."

All three show the line number of the failed assertion and the expression that failed, making these nicely self-documenting.

assert.bas(3): assertion failed at __FB_MAINPROC__: a+a=5
Ha, no.

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:

func assert(t bool, s string) {
	if !t {
		panic(s)
	}
}
//…
	assert(c == 0, "some text here")

(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.)

J

J can load scripts expecting any non-assigned noun result to be all 1's. If the file tautology_script.ijs contains

NB. demonstrate properties of arithmetic
'A B C' =: 3 ?@$ 0   NB. A B and C are random floating point numbers in range [0, 1).
((A + B) + C) -: (A + (B + C))  NB. addition associates
(A + B) -: (B + A)              NB. addition commutes
(A * B) -: (B * A)              NB. scalar multiplication commutes
(A * (B + C)) -: ((A * B) + (A * C)) NB. distributive property

we could load it into a session as 0!:3<'tautology_script.ijs' with result of 1, because the expressions match (-:). Were a sentence to fail the result would be 0, as for example replacing multiplication with matrix product and A B and C with square matrices of same size.

In next example the assertion both tests substitute when the script loads and shows how to use substitute. Infinity (_) replaces the zeros in the y argument, and the x argument is the vector zero infinity.

substitute =: 4 : '[&.((y~:{.x)&(#!.({:x)))y'
assert _ 1 1 _ 2 -: 0 _ substitute 0 1 1 0 2


Pre-condition adverbs with example:

Positive =: adverb define
 'non-positive' assert *./ , y > 0
 u y
)
Integral =: adverb define
 'non-integral' assert (-: <.) y
 u y
)
display =: smoutput :[:
display_positive_integers =: display Integral Positive

   display 1 3 8
1 3 8
   display_positive_integers 1 3 8
1 3 8
   display 1x1 _1p1 
2.71828 _3.14159
   display_positive_integers 1x1 _1p1 
|non-positive: assert
|   'non-positive'    assert*./,y>0

As a post-condition, and this is contrived because a better definition of exact_factorial would be !@:x: ,

IntegralResult =: adverb define
 RESULT =. u y
 'use extended precision!' assert (<datatype RESULT) e. ;:'extended integer'
 RESULT
:
 RESULT =. x u y
 'use extended precision!' assert (<datatype RESULT) e. ;:'extended integer'
 RESULT
)

exact_factorial =: !IntegralResult

   !50   
3.04141e64         
   !50x
30414093201713378043612608166064768844377641568960512000000000000
   exact_factorial 50x
30414093201713378043612608166064768844377641568960512000000000000
   exact_factorial 50
|use extended precision!: assert
|   'use extended precision!'    assert(<datatype RESULT)e.;:'extended integer'

One could assert an invariant in quicksort such that following the split the maximum of the small group is less than the minimum of the large group:

assert (>./LEFT) < (<./RIGHT)

Java

The -ea or -enableassertions option must be passed to the VM when running the application for this to work.
Example taken from Perceptron task.

(...)
int feedForward(double[] inputs) {
    assert inputs.length == weights.length : "weights and input length mismatch";

    double sum = 0;
    for (int i = 0; i < weights.length; i++) {
        sum += inputs[i] * weights[i];
    }
    return activate(sum);
}
(...)

jq

Library: Jq/assert.jq
Works with: jq

jq does not currently support assertions natively though they (and design by contract) can be simulated as here, using a jq module.

The "assert.jq" module allows assertion checking to be turned on or off; in addition, execution can be continued or terminated after an assertion violation is detected.

In the following, it is assumed the "debug" mode of assertion checking has been used, e.g. via the invocation: jq --arg assert debug

This mode allows execution to continue after an assertion violation has been detected.

include "rc-assert" {search: "."};  # or use the -L command-line option

def averageOfAbsolutes:
  . as $values
  # pre-condition
  | assert(type == "array" and length > 0 and all(type=="number");
           "input to averageOfAbsolutes should be a non-empty array of numbers.")
  | (map(length) | add/length) as $result
  # post-condition
  | assert($result >= 0; 
           $__loc__ + { msg: "Average of absolute values should be non-negative."} )
  | $result;

[1, 3], ["hello"]
| averageOfAbsolutes
Output:

Invocation: jq -n --arg assert debug -f assertions.jq

2
["DEBUG:","assertion violation @ input to averageOfAbsolutes should be a non-empty array of numbers. => false"]
5

Julia

The @assert macro is used for assertions in Julia.

function volumesphere(r)
    @assert(r > 0, "Sphere radius must be positive")
    return π * r^3 * 4.0 / 3.0
end

Kotlin

// version 1.1.2
// requires -ea JVM option

fun main(args: Array<String>) {
    assert(args.size > 0)  { "At least one command line argument must be passed to the program" }
    println("The following command line arguments have been passed:")
    for (arg in args) println(arg)
}
Output:

When run without passing command line arguments:

Exception in thread "main" java.lang.AssertionError: At least one command line argument must be passed to the program

When run passing 1 and 2 as command line arguments:

The following command line arguments have been passed:
1
2

Nim

Nim provides two kind of assertions: assertions which can be deactivated by compiling without checks and assertions which cannot be deactivated.

The first kind takes the form: assert boolean_expression with a default message or assert boolean_expression, message when with want a specific message. For the second kind, assert is simply replaced with doAssert.

Assertions may be used anywhere, either as preconditions, post-conditions or invariants.

Here is an example:

import math

func isqrt(n: int): int =
  assert n >= 0, "argument of “isqrt” cannot be negative"
  int(sqrt(n.toFloat))

If the assertion is not true, the program terminates in error with the exception AssertionDefect:

Error: unhandled exception: test.nim(2, 10) `n >= 0` argument of “isqrt” cannot be negative [AssertionDefect]

Note also that, in this case, rather than using an assertion, we could have simply specified that “n” must be a natural:

import math

func isqrt(n: Natural): int =
  int(sqrt(n.toFloat))

If the argument is negative, we get the following error:

Error: unhandled exception: value out of range: -1 notin 0 .. 9223372036854775807 [RangeDefect]

Perl

Translation of: Raku
# 20201201 added Perl programming solution

use strict;
use warnings;

package MessageMultiplier;

use Class::Contract;
use Test::More tests => 2;
use Test::Exception;

contract {

   attr 'multiplier' => 'SCALAR';
   attr 'message'    => 'SCALAR';

   ctor 'new';
      impl { ( ${self->multiplier}, ${self->message} ) = @_ };

   method 'execute';
      pre  { ${self->multiplier} > 1 and length ${self->message} > 0 };
      impl { print ${self->message} x ${self->multiplier} , "\n" };
};

MessageMultiplier->new(2,'A')->execute;
dies_ok { MessageMultiplier->new(1,'B')->execute };
dies_ok { MessageMultiplier->new(3, '')->execute };
Output:
1..2
AA
ok 1
ok 2

Phix

User defined types can be used to directly implement design by contract, and disabled by "without type_check".

type hour(object x)
    return integer(x) and x>=0 and x<=23
end type
hour h
h = 1   -- fine
h = 26  -- bad (desktop/Phix only)
Output:
C:\Program Files (x86)\Phix\test.exw:6
type check failure, h is 26

Type check failures can also be caught and processed just like any other exception.

You can also (since 0.8.2) use standard assert statemnents, eg

integer fn = -1 -- (try also 1)
assert(fn!=-1,"cannot open config file")

Racket

The function and it's contract are a "translation" of "D".

The Racket Guide introduces contracts here [1]

The Racket Reference defines contracts here [2]

Note that the examples catch contract blame exceptions -- which, if uncaught are enough to halt a program; making them quite assertive.

This example is extremely surface-scratching.

#lang racket
(require racket/contract)

;; This is the contract we will use.
;; "->"                   It is a function
;; (cons/c real?          That takes a list of at least one real (cons/c x (listof x)) means that an x
;;  (listof real?))       must occur before the rest of the list
;; (or/c zero? positive?) returns a non-negative number (for which there is no simpler contract that I
;;                        know of
(define average-of-absolutes/c
  (-> (cons/c real? (listof real?)) (or/c zero? positive?)))

;; this does what it's meant to
(define/contract (average-of-absolutes num-list)
  average-of-absolutes/c
  (/ (apply + (map abs num-list)) (length num-list)))

;; this will return a non-positive real (which will break the contract)
(define/contract (average-of-absolutes:bad num-list)
  average-of-absolutes/c
  (- (/ (apply + (map abs num-list)) (length num-list))))

(define (show-blame-error blame value message)
  (string-append   "Contract Violation!\n"
                   (format "Guilty Party: ~a\n" (blame-positive blame))
                   (format "Innocent Party: ~a\n" (blame-negative blame))
                   (format "Contracted Value Name: ~a\n" (blame-value blame))
                   (format "Contract Location: ~s\n" (blame-source blame))
                   (format "Contract Name: ~a\n" (blame-contract blame))
                   (format "Offending Value: ~s\n" value)
                   (format "Offense: ~a\n" message)))
(current-blame-format show-blame-error)

(module+ test
  ;; a wrapper to demonstrate blame
  (define-syntax-rule (show-contract-failure body ...)
    (with-handlers [(exn:fail:contract:blame?
                     (lambda (e) (printf "~a~%" (exn-message e))))]
                    (begin body ...)))
  
  (show-contract-failure (average-of-absolutes '(1 2 3)))
  (show-contract-failure (average-of-absolutes '(-1 -2 3)))
  
  ;; blame here is assigned to this test script: WE're providing the wrong arguments
  (show-contract-failure (average-of-absolutes 42))
  (show-contract-failure (average-of-absolutes '()))

  ;; blame here is assigned to the function implementation: which is returning a -ve value
  (show-contract-failure (average-of-absolutes:bad '(1 2 3)))
  (show-contract-failure (average-of-absolutes:bad '(-1 -2 3)))
  
  ;; blame here is assigned to this test script: since WE're providing the wrong arguments, so
  ;; the bad function doesn't have a chance to generate an invalid reply
  (show-contract-failure (average-of-absolutes:bad 42))
  (show-contract-failure (average-of-absolutes:bad '())))
Output:
2
2
Contract Violation!
Guilty Party: ...\Assertions_in_design_by_contract.rkt
Innocent Party: (function average-of-absolutes)
Contracted Value Name: average-of-absolutes
Contract Location: #(struct:srcloc "...\\Assertions_in_design_by_contract.rkt" 28 18 1037 20)
Contract Name: (-> (cons/c real? (listof real?)) (or/c zero? positive?))
Offending Value: 42
Offense: expected: pair?
  given: 42

Contract Violation!
Guilty Party: ...\Assertions_in_design_by_contract.rkt
Innocent Party: (function average-of-absolutes)
Contracted Value Name: average-of-absolutes
Contract Location: #(struct:srcloc "...\\Assertions_in_design_by_contract.rkt" 28 18 1037 20)
Contract Name: (-> (cons/c real? (listof real?)) (or/c zero? positive?))
Offending Value: ()
Offense: expected: pair?
  given: ()

Contract Violation!
Guilty Party: (function average-of-absolutes:bad)
Innocent Party: ...\Assertions_in_design_by_contract.rkt
Contracted Value Name: average-of-absolutes:bad
Contract Location: ...\\Assertions_in_design_by_contract.rkt" 33 18 1238 24)
Contract Name: (-> (cons/c real? (listof real?)) (or/c zero? positive?))
Offending Value: -2
Offense: promised: (or/c zero? positive?)
  produced: -2

Contract Violation!
Guilty Party: (function average-of-absolutes:bad)
Innocent Party: ...\Assertions_in_design_by_contract.rkt
Contracted Value Name: average-of-absolutes:bad
Contract Location: #(struct:srcloc "...\\Assertions_in_design_by_contract.rkt" 33 18 1238 24)
Contract Name: (-> (cons/c real? (listof real?)) (or/c zero? positive?))
Offending Value: -2
Offense: promised: (or/c zero? positive?)
  produced: -2

Contract Violation!
Guilty Party: ...\Assertions_in_design_by_contract.rkt
Innocent Party: (function average-of-absolutes:bad)
Contracted Value Name: average-of-absolutes:bad
Contract Location: #(struct:srcloc "...\\Assertions_in_design_by_contract.rkt" 33 18 1238 24)
Contract Name: (-> (cons/c real? (listof real?)) (or/c zero? positive?))
Offending Value: 42
Offense: expected: pair?
  given: 42

Contract Violation!
Guilty Party: ...\Assertions_in_design_by_contract.rkt
Innocent Party: (function average-of-absolutes:bad)
Contracted Value Name: average-of-absolutes:bad
Contract Location: #(struct:srcloc "...\\Assertions_in_design_by_contract.rkt" 33 18 1238 24)
Contract Name: (-> (cons/c real? (listof real?)) (or/c zero? positive?))
Offending Value: ()
Offense: expected: pair?
  given: ()

Raku

(formerly Perl 6)

Works with: Rakudo version 2018.05

Most of theses entries seem to have missed the point. This isn't about how to implement or use assertions, it is about how the language uses design-by-contract to help the programmer get correct results.

Raku doesn't have an assert routine in CORE. You could easily add one; several modules geared toward unit testing supply various "assertion" routines, though I'm not aware of any actually specifically named "assert()".

Raku core has subroutine signatures, multi-dispatch and exceptions to implement design-by-contract.

Subroutine signature allow the programmer to make the parameters supplied to a routine be checked to make sure they are the of correct quantity, type, and value and can constrain the returned value(s) to a particular type. See the below snippet for a brief demonstration. Raku does some static analysis to trap errors at compile time, but traps many errors at run time since it is often impossible to tell if a variable is of the correct type before the program is run.

When Raku encounters a design-by-contract violation, it will fail with an error message telling where the problem occurred, what it expected and what it actually got. Some failures are trappable and resumeable. Failures may be trapped by adding a CATCH { } block in the current scope. Failures will transfer execution to the CATCH block where the failure may be analysed and further action taken. Depending on the failure type, execution may be resumable. Some failures cause execution to halt unavoidably.

In this snippet, the routine repeat takes one Integer that must be greater than 1, a String and returns a String. (Note that as written, it is incorrect since it actually returns a boolean.)

sub repeat ( Int $repeat where * > 1, Str $message, --> Str ) {
    say $message x $repeat;
    True # wrong return type
}

repeat( 2, 'A' ); # parameters ok, return type check error

repeat( 4, 2 ); # wrong second parameter type

repeat( 'B', 3 ); # wrong first (and second) parameter type

repeat( 1, 'C' ); # constraint check fail

repeat( ); # wrong number of parameters

CATCH {
    default {
        say "Error trapped: $_";
        .resume;
    }
}
Output:
AA
Error trapped: Type check failed for return value; expected Str but got Bool (Bool::True)
Error trapped: Type check failed in binding to parameter '$message'; expected Str but got Int (2)
Error trapped: Type check failed in binding to parameter '$repeat'; expected Int but got Str ("B")
Error trapped: Constraint type check failed in binding to parameter '$repeat'; expected anonymous constraint to be met but got Int (1)
Error trapped: Too few positionals passed; expected 2 arguments but got 0
This exception is not resumable
  in block  at contract.p6 line 19
  in block <unit> at contract.p6 line 14

REXX

This is just a simple method of   assertion;   more informative messages could be added in the   assertion   routine.
A   return   statement could've been used instead of an   exit   statement to continue processing.

/*REXX program demonstrates a  method  on how to use  assertions in design  by contract.*/
parse arg top .                                  /*obtain optional argument from the CL.*/
if top=='' | top==","  then top= 100             /*Not specified?  Then use the default.*/
_= left('', 9)                                   /*_:  contains 9 blanks for SAY passing*/
                        w= length(top) + 1       /*W:  is used for aligning the output. */
      do #=1  for 666                            /*repeat for a devilish number of times*/
      a= random(1, top)                          /*generate a random number  (1 ──► TOP)*/
      b= random(1,   a)                          /*    "    "    "      "    (1 ──►   A)*/
      c= a - b                                   /*compute difference between  A and B. */
      say _'a='right(a, w)_"b="right(b, w)_'c='right(c, w)_"sum="right(sumABC(a, b, c), w)
      call assert  date('Weekday') \== "Monday"  /*shouldn't execute this pgm on Monday.*/
      call assert  time('H')<9  |  time("H")>15  /*    ··· and not during banking hours.*/
      call assert  c>0                           /*The value of   C   must be positive. */
      end   /*#*/
exit 0                                           /*stick a fork in it,  we're all done. */
/*──────────────────────────────────────────────────────────────────────────────────────*/
assert: if arg(1)  then return 1;       say      /*if true,  then assertion has passed. */
        say 'assertion failed on line ' sigL " with: "  subword(space(sourceline(sigl)),2)
        say;   say '# index= '  #
        say 'ASSERT is exiting.';       exit 13
/*──────────────────────────────────────────────────────────────────────────────────────*/
sumABC: procedure; parse arg x,y,z; return x+y+z /*Sum three arguments.  Real easy work.*/
output   when using the default input:
         a=  12         b=   5         c=   7         sum=  24
         a=  88         b=  77         c=  11         sum= 176
         a=  35         b=  26         c=   9         sum=  70
         a=  33         b=   9         c=  24         sum=  66
         a=  90         b=  31         c=  59         sum= 180
         a=  64         b=   9         c=  55         sum= 128
         a=  82         b=  18         c=  64         sum= 164
         a=   6         b=   4         c=   2         sum=  12
         a=  85         b=  72         c=  13         sum= 170
         a=  74         b=  49         c=  25         sum= 148
         a=  31         b=  14         c=  17         sum=  62
         a=  58         b=  48         c=  10         sum= 116
         a=  64         b=  59         c=   5         sum= 128
         a=  53         b=   1         c=  52         sum= 106
         a=  54         b=  22         c=  32         sum= 108
         a=  36         b=   9         c=  27         sum=  72
         a=   2         b=   2         c=   0         sum=   4

assertion failed on line  13  with:  assert c>0 /*The value of C must be positive. */

# index=  17
ASSERT is exiting.

Ruby

require 'contracts'
include Contracts

Contract Num => Num
def double(x)
  x * 2
end

puts double("oops")
Output:
./contracts.rb:34:in `failure_callback': Contract violation: (RuntimeError)
    Expected: Contracts::Num,
    Actual: "oops"
    Value guarded in: Object::double
    With Contract: Contracts::Num, Contracts::Num
    At: main.rb:6 

Scala

Scala provides runtime assertions like Java: they are designed to be used by static analysis tools however the default compiler doesn’t perform such analyses by default. The Scala assertions (assume, require, assert, ensuring) are Predef library methods that are enabled by default and can be disabled using the -Xdisable-assertions runtime flag, unlike Java where assertions are disabled by default and enabled with a runtime flag. It is considered poor form to rely on assertions to validate arguments, because they can be disabled. An appropriate informative runtime exception (e.g. NullPointerException or IllegalArgumentException) should be thrown instead.

object AssertionsInDesignByContract extends App {
    /**
     * @param ints a non-empty array of integers
     * @return the mean magnitude of the array's elements.
     */
    def averageOfMagnitudes(ints: Array[Int]) = {
        // assertions for static analysis / runtime protoyping:
        assume(ints != null, "array must not be null")
        require(ints.length > 0, "array must be non-empty")
        // runtime exceptions when assertions are disabled:
        if (ints.length < 1) throw new IllegalArgumentException("Cannot find the average of an empty array")
        // note, the above line can implicitly throw a NullPointerException too
        val abs = ints.map(Math.abs)
        val mean = Math.round(abs.sum.toDouble / ints.length)
        assert(Math.abs(mean) >= abs.min && Math.abs(mean) <= abs.max, "magnitude must be within range")
        mean
    } ensuring(_ >= 0, "result must be non-negative (possible overflow)")

    println(averageOfMagnitudes(Array(1))) // 1
    println(averageOfMagnitudes(Array(1,3))) // 2
    println(averageOfMagnitudes(null)) // java.lang.AssertionError: assumption failed: array must not be null
    println(averageOfMagnitudes(Array())) // java.lang.IllegalArgumentException: requirement failed: array must be non-empty
    println(averageOfMagnitudes(Array(Integer.MAX_VALUE, Integer.MAX_VALUE))) // java.lang.AssertionError: assertion failed: magnitude must be within range
    println(averageOfMagnitudes(Array(Integer.MAX_VALUE, 1))) // java.lang.AssertionError: assertion failed: result must be non-negative (possible overflow)
}

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
}

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

Wren

Translation of: D
Library: Wren-assert

Wren doesn't support assertions natively though they (and design by contract) can be simulated using a library.

import "./assert" for Assert
import "./math" for Nums

// Assert.disabled = true

var averageOfAbsolutes = Fn.new { |values|
    // pre-condition
    Assert.ok(values.count > 0, "Values list must be non-empty.")

    var result = Nums.mean(values.map { |v| v.abs })
    // post-condition
    Assert.ok(result >= 0, "Average of absolute values should be non-negative.")
    return result
}

class Foo {
    construct new(x) {
        _x = x
        checkInvariant_()
    }

    x { _x }
    x=(v) {
        _x = v
        checkInvariant_()
    }

    inc {
        // no need to check invariance here
        _x = _x + 1
    }

    checkInvariant_() {
        Assert.ok(_x >= 0, "Field 'x' must be non-negative.")
    }
}

System.print(averageOfAbsolutes.call([1, 3]))
var f = Foo.new(-1)
f.inc
System.print(f.x)
Output:

With assertions enabled:

2
Field 'x' must be non-negative.
[./assert line 225] in fail(_)
[./assert line 71] in ok(_,_)
[./assertions_in_DBC line 34] in checkInvariant_()
[./assertions_in_DBC line 19] in init new(_)
[./assertions_in_DBC line 20] in 
[./assertions_in_DBC line 39] in (script)

or with assertions disabled (un-comment line 4):

2
0

Z80 Assembly

There are no built-in assertions, error handlers, etc. at the hardware level. The closest you can get is a function conditionally returning early. For example, this function for multiplication checks if the second factor equals zero or 1 before attempting to multiply.

SmallMultiply:
;returns A = C * A
or a       ;compares A to zero
ret z      ;returns with the product A = C * 0 = 0.
dec a      ;sets zero flag if A equaled 1 prior to decrement, effectively comparing A to 1.
jr z, C_Times_One
ld b,a
ld a,c
loop_smallMultiply:
add c
djnz loop_smallMultiply
ret   ;returns A = C * A


C_Times_One:
ld a,c
ret  ;returns A = C

zkl

zkl has exceptions. The _assert_ keyword just wraps the AssertionError exception. _assert_ takes an expression and optional message. There are no pre/post conditionals.

fcn f(a){
   _assert_((z:=g())==5,"I wanted 5, got "+z)
}

Running the code throws an exception with file and line number:

Output:
VM#1 caught this unhandled exception:
   AssertionError : assert(foo.zkl:14): I wanted 5, got hoho