Assertions in design by contract: Difference between revisions

You '''cannot''' read the break flag this way:

pla

and #%00010000

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_Hi equ $21 ;this must be one byte higher than the previous address.

org $FFFA

=={{header|68000 Assembly}}==

Precondition example:

Postcondition examples:

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.

=={{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));

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

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;

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.

Type invariants can be specified using aspect clauses such as:

Dynamic_Predicate => Evens mod 2 = 0;

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.

{{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

write( averageOfAbsolutes( v, 2 ) )

end

{{out}}

<pre>

=={{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

Foo f;

f.inc;

{{out}}

<pre>2</pre>

=={{header|Eiffel}}==

{{trans|D}}

average_of_absolutes (values: ARRAY[INTEGER]): INTEGER

require

ensure

non_neg_result: Result >= 0

=={{header|Fortran}}==

LOGICAL CONDITION

CHARACTER*(*) MESSAGE

WRITE (6,*) MESSAGE

STOP "Oops. Confusion!"

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

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 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:

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 )

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

If someone disagrees and they ''really'' want to use an "assert" they can simply roll their own:

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

|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

| '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:

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";

return activate(sum);

}

=={{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

=={{header|Kotlin}}==

// requires -ea JVM option

println("The following command line arguments have been passed:")

for (arg in args) println(arg)

{{out}}

Here is an example:

func isqrt(n: int): int =

assert n >= 0, "argument of “isqrt” cannot be negative"

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

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

func isqrt(n: Natural): int =

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

=={{header|Perl}}==

{{trans|Raku}}

use strict;

MessageMultiplier->new(2,'A')->execute;

dies_ok { MessageMultiplier->new(1,'B')->execute };

{{out}}

<pre>1..2

=={{header|Phix}}==

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

<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: #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>

{{out}}

<pre>

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

<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>

=={{header|Racket}}==

This example is extremely surface-scratching.

#lang racket

(require racket/contract)

;; the bad function doesn't have a chance to generate an invalid reply

(show-contract-failure (average-of-absolutes:bad 42))

{{out}}

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

say $message x $repeat;

True # wrong return type

.resume;

}

{{out}}

<pre>AA

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.

parse arg top . /*obtain optional argument from the CL.*/

if top=='' | top=="," then top= 100 /*Not specified? Then use the default.*/

say 'ASSERT is exiting.'; exit 13

/*──────────────────────────────────────────────────────────────────────────────────────*/

{{out|output|text=&nbsp; when using the default input:}}

<pre>

=={{header|Ruby}}==

require 'contracts'

include Contracts

puts double("oops")

{{out}}

<pre>

=={{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

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]]} {

return $sock

This can be usefully mixed with Tcl 8.6's <code>try … finally …</code> built-in command.

{{libheader|Wren-assert}}

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

import "/math" for Nums

var f = Foo.new(-1)

f.inc

{{out}}

=={{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.

;returns A = C * A

or a ;compares A to zero

C_Times_One:

ld a,c

=={{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}}