Assertions in design by contract: Difference between revisions
m
→{{header|Wren}}: Minor tidy
No edit summary |
m (→{{header|Wren}}: Minor tidy) |
||
| (22 intermediate revisions by 7 users not shown) | |||
Line 7:
Show in the program language of your choice an example of the use of assertions as a form of documentation.
<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}}==
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:
<
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));
</syntaxhighlight>
The precondition above requires the array to be sorted to have more than one data element.
Line 21 ⟶ 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 => 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;
</syntaxhighlight>
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 ⟶ 108:
Type invariants can be specified using aspect clauses such as:
<
Dynamic_Predicate => Evens mod 2 = 0;
Line 42 ⟶ 118:
subtype Alternates is Days with
Static_Predicate => Alternates in Mon | Wed | Fri | Sun;
</syntaxhighlight>
The Dynamic_Predicate used for subtype Evens above specifies that each value of the subtype must be an even number.
Line 52 ⟶ 128:
{{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.
<
long real procedure averageOfAbsolutes( integer array values( * )
; integer value valuesLength
Line 72 ⟶ 148:
write( averageOfAbsolutes( v, 2 ) )
end
end.</
{{out}}
<pre>
Line 80 ⟶ 156:
=={{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.
<
double averageOfAbsolutes(in int[] values) pure nothrow @safe @nogc
Line 106 ⟶ 182:
Foo f;
f.inc;
}</
{{out}}
<pre>2</pre>
Line 112 ⟶ 188:
=={{header|Eiffel}}==
{{trans|D}}
<
average_of_absolutes (values: ARRAY[INTEGER]): INTEGER
require
Line 122 ⟶ 198:
ensure
non_neg_result: Result >= 0
end</
=={{header|Fortran}}==
Fortran offers no formal "assert" protocol, but there would be nothing to stop a programmer devising a subroutine such as <
LOGICAL CONDITION
CHARACTER*(*) MESSAGE
Line 131 ⟶ 207:
WRITE (6,*) MESSAGE
STOP "Oops. Confusion!"
END </
And then scattering through the source file lines such as <
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 <
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 ⟶ 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:
<
The macro <code>assert</code> will halt at runtime with an error message if its argument evaluates to zero:
<
assert( Pi < 3 )</
Finally, <code>assertwarn</code> is like <code>assert</code> but only prints an error message and continues running:
<
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.
Line 171 ⟶ 247:
If someone disagrees and they ''really'' want to use an "assert" they can simply roll their own:
<
if !t {
panic(s)
Line 178 ⟶ 254:
//…
assert(c == 0, "some text here")
</syntaxhighlight>
(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 ⟶ 260:
J can load scripts expecting any non-assigned noun result to be all 1's.
If the file tautology_script.ijs contains
<syntaxhighlight lang="j">
NB. demonstrate properties of arithmetic
'A B C' =: 3 ?@$ 0 NB. A B and C are random floating point numbers in range [0, 1).
Line 191 ⟶ 267:
(A * B) -: (B * A) NB. scalar multiplication commutes
(A * (B + C)) -: ((A * B) + (A * C)) NB. distributive property
</syntaxhighlight>
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.
<syntaxhighlight lang="j">
substitute =: 4 : '[&.((y~:{.x)&(#!.({:x)))y'
assert _ 1 1 _ 2 -: 0 _ substitute 0 1 1 0 2
</
Pre-condition adverbs with example:
<syntaxhighlight lang="j">
Positive =: adverb define
'non-positive' assert *./ , y > 0
Line 223 ⟶ 299:
|non-positive: assert
| 'non-positive' assert*./,y>0
</syntaxhighlight>
As a post-condition, and this is contrived because a better definition of exact_factorial would be !@:x: ,
<syntaxhighlight lang="j">
IntegralResult =: adverb define
RESULT =. u y
Line 248 ⟶ 324:
|use extended precision!: assert
| 'use extended precision!' assert(<datatype RESULT)e.;:'extended integer'
</syntaxhighlight>
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 ⟶ 332:
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]].
<
int feedForward(double[] inputs) {
assert inputs.length == weights.length : "weights and input length mismatch";
Line 266 ⟶ 342:
return activate(sum);
}
(...)</
=={{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}}==
The @assert macro is used for assertions in Julia.
<
@assert(r > 0, "Sphere radius must be positive")
return π * r^3 * 4.0 / 3.0
end
</syntaxhighlight>
=={{header|Kotlin}}==
<
// requires -ea JVM option
Line 284 ⟶ 400:
println("The following command line arguments have been passed:")
for (arg in args) println(arg)
}</
{{out}}
Line 297 ⟶ 413:
2
</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}}==
{{trans|Raku}}
<
use strict;
Line 326 ⟶ 471:
MessageMultiplier->new(2,'A')->execute;
dies_ok { MessageMultiplier->new(1,'B')->execute };
dies_ok { MessageMultiplier->new(3, '')->execute };</
{{out}}
<pre>1..2
Line 335 ⟶ 480:
=={{header|Phix}}==
User defined types can be used to directly implement design by contract, and disabled by "without type_check".
<!--<syntaxhighlight lang="phix">-->
<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>
<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>
<span style="color: #008080;">end</span> <span style="color: #008080;">type</span>
<span style="color: #000000;">hour</span> <span style="color: #000000;">h</span>
<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>
<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}}
<pre>
Line 349 ⟶ 496:
You can also (since 0.8.2) use standard assert statemnents, eg
<!--<syntaxhighlight lang="phix">(phixonline)-->
<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}}==
Line 366 ⟶ 516:
This example is extremely surface-scratching.
<
#lang racket
(require racket/contract)
Line 421 ⟶ 571:
;; 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 '())))</
{{out}}
Line 501 ⟶ 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.)
<syntaxhighlight lang="raku"
say $message x $repeat;
True # wrong return type
Line 521 ⟶ 671:
.resume;
}
}</
{{out}}
<pre>AA
Line 535 ⟶ 685:
=={{header|REXX}}==
This is just a simple method of ''assertion''; more informative messages could be added in the '''assertion''' routine.
<br>A '''return''' statement could've been used instead of an '''exit''' statement to continue processing.
<
parse arg top . /*obtain optional argument from the CL.*/
if top=='' | top=="," then top=
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)
b= random(1, a)
c= a -
say
call assert date('Weekday') \== "Monday"
call assert time('H')<9 | time("H")>15
call assert c>0 /*The value of C must be positive. */
end /*#*/
exit
/*──────────────────────────────────────────────────────────────────────────────────────*/
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)),
say; say '# index= ' #
say 'ASSERT is exiting.';
/*──────────────────────────────────────────────────────────────────────────────────────*/
<pre>
a= 88 b= 77 c=
a= 33 b= 9 c=
a= 64 b= 9 c=
a= 6 b= 4 c=
a= 74 b= 49 c=
a= 58 b= 48 c=
a= 53 b= 1 c=
a= 36 b= 9 c=
assertion failed on line 13 with: assert c>0 /*The value of C must be positive. */
# index=
ASSERT is exiting.
</pre>
=={{header|Ruby}}==
<
require 'contracts'
include Contracts
Line 602 ⟶ 746:
puts double("oops")
</syntaxhighlight>
{{out}}
<pre>
Line 615 ⟶ 759:
=={{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.
<
/**
* @param ints a non-empty array of integers
Line 639 ⟶ 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, 1))) // java.lang.AssertionError: assertion failed: result must be non-negative (possible overflow)
}</
=={{header|Tcl}}==
<
proc require {expression message args} {
if {![uplevel 1 [list expr $expression]]} {
Line 668 ⟶ 812:
return $sock
}</
This can be usefully mixed with Tcl 8.6's <code>try … finally …</code> built-in command.
Line 678 ⟶ 822:
PRECONDITION FAILED: port must be valid for client
</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}}==
zkl has exceptions. The _assert_ keyword just wraps the AssertionError exception. _assert_ takes an expression and optional message.
There are no pre/post conditionals.
<
_assert_((z:=g())==5,"I wanted 5, got "+z)
}</
Running the code throws an exception with file and line number:
{{out}}
| |||