Testing pre- and post-condition directly in the signature of a function.

pre-and-postcondition.raku

#!/usr/bin/env raku

# Implementing the function
# some-function$:\mathbb{Z}\times\mathbb{N} \to \{1,2,\dots,10\}, (a,b) \mapsto a + b $ where $a \equiv_2 (a+b) \equiv_2 1$

#| applied to the co-domain of &some-function()
subset Allowed-Returns of UInt where * ∈ 1..10;

#|« Pre- und Post-Condition in signature demonstration!
    * a ∈ ℤ ∧ a is odd
    * b ∈ ℕ ∧ (a + b) is odd
    * return value ∈ 1..10
»
sub some-function(Int $a where * mod 2,
                  UInt $b where { ($a + $b) mod 2 },
		--> Allowed-Returns ) {
	$a + $b
}
#=«
dies-ok { some-function(1+i,7)    }, "(a=1+i,b=7)-> a ∉ ℤ";
dies-ok { some-function(2,7)      }, "(a=2,b=7)  -> a not odd";
dies-ok { some-function(3,-2)     }, "(a=3,b=-2) -> b ∉ ℕ";
dies-ok { some-function(1,9)      }, "(a=1,b=9)  -> a+b not odd";
dies-ok { some-function(1,10)     }, "(a=1,b=10) -> a+b ∉ 1..10";
nok       some-function(1,6) == 9  , "(a=1,b=6)  -> all pre- and post-conditions met, result incorrect";
ok        some-function(1,8) == 9  , "(a=1,b=8)  -> all pre- and post-conditions met, result correct";
»

# run tests in trailing declarator block quick (and dirty)
use Test;               # ok nok is isnt is-approx is-deeply cmp-ok like unlike dies-ok etc. : https://docs.raku.org/type/Test
use MONKEY-SEE-NO-EVAL; # execute an arbitrary string as Raku/Python/Perl/etc. using EVAL

for &some-function.WHY.trailing.split(";") -> $single-test {
  EVAL $single-test
}