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

[Olwen Morgan]

OK - I'll dig the code out but not right now as I've something more 
urgent to do.


Olwen


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/592d3f6e/attachment.html>