search

ada-ros / ada4ros2

Ada binding and tools for ROS2 - workspace overlay and documentation
GNU Lesser General Public License v3.0
21 stars 3 forks source link

SPARK #47

Open dorkamotorka opened 3 years ago

dorkamotorka commented 3 years ago

Can integration of Ada and ROS2 be used/tested with SPARK?

mosteo commented 3 years ago

I have minimal experience with SPARK, but my understanding is that compilation is the same, and so it should work for SPARK client code. As for verification, my intuition is that running the prover after setting the appropriate environment should be doable too.

The Ada library itself is heavily reliant on the C client library, so there are lots of hidden pointers. I'm unsure about how hard would be to provide some SPARK assurances on RCLAda itself as it is now. There should be no heap allocations after initialization in RCLAda though.

We have a mid-term plan on trying to implement some algorithm with some level of SPARK assurance, so definitely this is something we are going to attempt at some point.

dorkamotorka commented 3 years ago

Thanks for a lengthy answer.