[SystemSafety] More on my contretemps with PBL ...
Roderick Chapman
rod at proteancode.com
Fri Jul 10 14:04:46 CEST 2020
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>
More information about the systemsafety
mailing list