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

[Roderick Chapman]

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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200710/1a2668f7/attachment.html>