InvariantsCore
This file defines
invariant
, which allows creating and combining invariants and should cover most use cases. It also defines
check
for running an innput against an invariant. ##
invariant
The basic method simply returns an
Invariant
:
invariant
(
fn
,
title
::
String
;
kwargs
...
)
=
Invariant
(
fn
,
title
;
kwargs
...
)
invariant
can be called on a vector of invariants, creating an invariant that logically composes them (either AND or OR):
function
invariant
(
title
,
invariants
::
AbstractVector
{
<:
AbstractInvariant
}
;
kwargs
...
)
invariant
(
title
,
invariants
,
all
;
kwargs
...
)
end
function
invariant
(
title
,
invariants
::
AbstractVector
{
<:
AbstractInvariant
}
,
::
typeof
(
all
)
;
kwargs
...
)
AllInvariant
(
invariants
,
title
;
kwargs
...
)
end
function
invariant
(
title
,
invariants
::
AbstractVector
{
<:
AbstractInvariant
}
,
::
typeof
(
any
)
;
kwargs
...
)
AnyInvariant
(
invariants
,
title
;
kwargs
...
)
end
invariant
can also wrap an invariant, changing some of its attributes. For a general
AbstractInvariant
, this will return a
WrapInvariant
:
function
invariant
(
inv
::
AbstractInvariant
;
title
=
nothing
,
inputfn
=
identity
,
description
=
nothing
,
format
=
nothing
)
if
isnothing
(
title
)
&&
inputfn
===
identity
&&
isnothing
(
description
)
&&
isnothing
(
format
)
return
inv
end
return
WrapInvariant
(
inv
,
title
,
description
,
inputfn
,
format
)
end
function
invariant
(
inv
::
Invariant
;
title
=
nothing
,
inputfn
=
identity
,
description
=
nothing
,
format
=
nothing
)
return
Invariant
(
inv
.
fn
,
isnothing
(
title
)
?
inv
.
title
:
title
,
isnothing
(
description
)
?
inv
.
description
:
description
,
inputfn
===
identity
?
inv
.
inputfn
:
inputfn
∘
inv
.
inputfn
,
isnothing
(
format
)
?
inv
.
format
:
format
)
end
check
function
check
(
invariant
,
input
)
res
=
satisfies
(
invariant
,
input
)
return
CheckResult
(
invariant
,
res
)
end
check
(
::
Type
{
Bool
}
,
invariant
,
input
)
=
isnothing
(
satisfies
(
invariant
,
input
)
)
struct
CheckResult
{
I
,
R
}
invariant
::
I
result
::
R
end
Base
.
convert
(
::
Type
{
Bool
}
,
checkres
::
CheckResult
)
=
isnothing
(
checkres
.
result
)
function
Base
.
show
(
io
::
IO
,
checkres
::
CheckResult
{
<:
I
,
Nothing
}
)
where
{
I
}
print
(
io
,
"
\e[32m✔ Invariant satisfied:\e[0m
"
)
print
(
io
,
title
(
checkres
.
invariant
)
)
end
function
Base
.
show
(
io
::
IO
,
checkres
::
CheckResult
)
print
(
io
,
"
\e[1m\e[31m⨯ Invariant not satisfied:\e[0m\e[1m
"
)
print
(
io
,
title
(
checkres
.
invariant
)
)
print
(
io
,
"
\e[22m\n
"
)
errormessage
(
io
,
checkres
.
invariant
,
checkres
.
result
)
end
For cases where violating an invariant should lead to an error be thrown, use
check_throw
:
function
check_throw
(
invariant
,
input
)
res
=
satisfies
(
invariant
,
input
)
isnothing
(
res
)
&&
return
throw
(
InvariantException
(
invariant
,
res
)
)
end
struct
InvariantException
{
I
<:
AbstractInvariant
,
M
}
invariant
::
I
msg
::
M
end
function
Base
.
showerror
(
io
::
IO
,
e
::
InvariantException
)
println
(
io
,
"
Invariant violated!
"
)
errormessage
(
io
,
e
.
invariant
,
e
.
msg
)
end