<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<p>OK - I'll dig the code out but not right now as I've something
more urgent to do.</p>
<p><br>
</p>
<p>Olwen</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 10/07/2020 13:04, Roderick Chapman
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:7454a85d-3c4d-4bd4-3357-4cfc00dad1ef@proteancode.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<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><br>
</p>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
The System Safety Mailing List
<a class="moz-txt-link-abbreviated" href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE">systemsafety@TechFak.Uni-Bielefeld.DE</a>
Manage your subscription: <a class="moz-txt-link-freetext" href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></pre>
</blockquote>
</body>
</html>