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.

 

 

Precondition example:

 

Postcondition examples:

TRAPV ;no overflow is expected, so if it occurs call the relevant trap.</syntaxhighlight>

 

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

 

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

 

Type invariants can be specified using aspect clauses such as:

Dynamic_Predicate => Evens mod 2 = 0;

 

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

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

=={{header|Eiffel}}==

{{trans|D}}

average_of_absolutes (values: ARRAY[INTEGER]): INTEGER

require

 

=={{header|Fortran}}==

LOGICAL CONDITION

CHARACTER*(*) MESSAGE

STOP "Oops. Confusion!"

END </syntaxhighlight>

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:

assert( Pi < 3 )</syntaxhighlight>

 

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 )

 

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

if !t {

panic(s)

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

 

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

 

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

IntegralResult =: adverb define

RESULT =. u y

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

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

 

=={{header|Kotlin}}==

// requires -ea JVM option

 

Here is an example:

 

 

func isqrt(n: int): int =

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 =

=={{header|Perl}}==

{{trans|Raku}}

 

use strict;

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

 

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>

This example is extremely surface-scratching.

 

#lang racket

(require racket/contract)

 

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

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.*/

 

=={{header|Ruby}}==

require 'contracts'

include Contracts

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

 

=={{header|Tcl}}==

proc require {expression message args} {

if {![uplevel 1 [list expr $expression]]} {

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

 

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

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)

}</syntaxhighlight>