[SystemSafety] More on my contretemps with PBL ...

[Martyn Thomas]

I shall be interested to see the formal specification against which
'correctness' could be assured. I suspect there may be a category
mistake here.

Martyn

On 10/07/2020 13:04, Roderick Chapman wrote:
> On 10/07/2020 00:36, Olwen Morgan wrote:
>> 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.
>
> I can help with that... we can set it up in my GitHub account and
> share results here.
>
>  - Rod
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200710/fa3b26ac/attachment.html>