<html>

  <head>

    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">

  </head>

  <body>

    <div class="moz-cite-prefix">On 10/07/2020 00:36, Olwen Morgan

      wrote:<br>

    </div>

    <blockquote type="cite"

      cite="mid:221a3e19-85c7-54b4-a89c-a0671d85307a@phaedsys.com">Somewhere

      or other I have code for this generator in C complying with C90.

      I'm sure that it would readily transliterate into SPARK Ada and

      I'd be interested to learn what the capability of the SPARK tools

      would be to prove functional correctness.</blockquote>

    <p><font size="+1">I can help with that... we can set it up in my

        GitHub account and share results here.</font></p>

    <p><font size="+1"> - Rod</font></p>

    <p><font size="+1"></font><br>

    </p>

  </body>

</html>