Start with this:
test_assert(x: int) =
assert(x > 5)
echo "success"
var a = 5
test_assert(a)
Run
That fails to catch the error at compile time, _even though the value of ``a``
is known at compile time_.
Compare this to Spark 2014:
Ada.Text_IO; use Ada.Text_IO;
procedure Test_Contract with Spark_Mode is
procedure Test(a: Integer) with Pre => (a > 5) is
begin
if a > 5 then Put_Line("Oops!"); end if;
end Test;
a: Integer := 5;
begin
Test(a);
end Test_Contract;
Run
When I run `gnatprove` on this, the static analysis reports the following:
-P/Users/user/common/Nim_code/test_assert/test_contract.gpr -j0
--ide-progress-bar --level=0 -u test_contract.adb
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
test_contract.adb:5:13: warning: subprogram "Test" has no effect
test_contract.adb:7:19: warning: no Global contract available for "Put_Line"
test_contract.adb:7:19: warning: assuming "Put_Line" has no effect on
global items
test_contract.adb:13:03: medium: precondition might fail (e.g. when a = 5)
Summary logged in
/Users/user/common/Nim_code/test_assert/obj/gnatprove/gnatprove.out
Run
I repeat: It would be **very bad** to discover the contract failed **in
mid-flight**.
