<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>I shall be interested to see the formal specification against
which 'correctness' could be assured. I suspect there may be a
category mistake here.<br>
</p>
<p>Martyn<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>