SPARK Verified Postfix Expression Calculator

General
1

I got inspired by @streaksu’s Ironclad work and @OneWingedShark’s idea to write a verified seedForth interpreter in SPARK. That seemed a bit large as a starting SPARK project, so I wrote a SPARK verified postfix expression calculator.

I had a great time doing this, so I might try to fork that calculator into a simple Forth interpreter. I don’t have formal methods training, but I wrote up my experience if anyone is curious.

I would really appreciate any guidance on the current code or related post from those with formal methods experience. The only reference I have right now is McCormick/Chapin’s “Building High Integrity Applications with SPARK” book, but that has been very helpful so far.

18 Likes
2

Nice project! I’d love to see you continue ^^

3

Thank you! Could you please also add the prover output to the README in GitHub - pyjarrett/postfix_calc: A verified postfix calculator? This way, other non-Ada users can see what it looks like without having to install and run anything.

2 Likes
4

Very nice!
Glad I was somewhat inspiring.
(Reading the article now.)

5

Regarding " Floating point simplifications", what I’ve found useful in CoAP-SPARK for proving floating point properties is the COLIBRI prover. It doesn’t come with the Alire distribution of gnatprove, but can be separately obtained from the GNAT Community 2021 edition. Then, just putting the binary on the path is enough to make gnatprove find it and use it when requested by the arguments. This workflow automating the proof process of my project is doing the downloand and extraction from GNAT Community.

1 Like
6

Hi Manu and everybody else,

you can download the Colibri and Colibri2 (still highly in beta) from their website: Colibri

Their repositories (where the binaries come from) are the following:

I am pointing this out as they are open source projects that have seen quite a bit of development since the GNAT Community pack was discontinued. I believe it may be also much easier to download the binaries (or compressed binary) directly and just put it into the Path. I have tested Colibri and it did not do much better than the others, but as @mgrojo points out, each solver has their strengths, and Colibri’s lies in numeric stuff rather than program flow or similar topics.

I hope this helps you all!
Best regards,
Fer

1 Like
7

Using the latest Colibri or Colibri2 releases from the repositories, as you mention, was my first approach, but they aren’t really compatible with gnatprove yet, as AdaCore confimed me through the GNAT Academic program. But the tool fails silently and you don’t see any difference. The working version is Colibri 2020.9, but building from source is not trivial. I finally discovered that the correct version was present in the latest Community Edition. The license is LGPL since 2020, so there are no possible worries about using or distributing it.

1 Like
8

Oh, that explains a few things I saw during my testing…

That is actually a bit surprising to me as all the tools are using Why3 and there are already four provers supported (Z3, alt-ergo, cvc5 and Coq with some tweaks…). Oh well… That is quite sad :confused: I know however that AdaCore was looking/working in Colibri, which is fully confirmed by the fact that it was distributed with the Community Edition…

1 Like