Re: My new post on dev.to about SPARK

[Simon Wright <simon@pushface.org>]

mockturtle <framefritti@gmail.com> writes:

> Recently I wrote a small binary search procedure for a software of
> mine.  Since I always wanted to start using SPARK, I thought that this
> could be a nice small problem to start playing around with SPARK.  The
> post on dev.to is about my experience.
>
> If you are curious
>
> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id

Interesting!

I thought to have a bit of a play with it, and I found that neither CE
2019 nor CE 2020 will prove as is, including "assertion might fail,
cannot prove Bottom < Top"; but it proves just fine with 
   type Element_Type is new Integer;
or
   subtype Element_Type is Integer;