Sebastian Ertel (Apr 29 2024 at 15:31): Sebastian Ertel (Apr 29 2024 at 15:31):Dear SSProvers,
What is the proper way to prove function correctness properties of code written in SSProve?
I found the interpreter examples.
In my case, the SSProve code has imports.
I cannot find a way to resolve them because the tactics all work on syntactic/semantic judgments of the pRHL.
Help would be very much appreciated, thanks a lot!
Sebastian Ertel (May 07 2024 at 07:09):I found my mistake.
Of course, the interpreter cannot resolve any imports. That would require a composition.
But as far as I'm aware, there is only package composition.
I'm currently not sure whether I can extract a procedure from a package but it sounds possible.
For the moment, I did the functional correctness in a slightly contrived form via an assert statement and an indistinguishability proof.
Works but it is certainly not very direct because I'm proving a functional correctness property using the indistinguishability proof machinery.
Sebastian Ertel (May 07 2024 at 07:10):(I would mark this as resolved but I can't since the topic is more than 7 days old. Maybe somebody else can do that for me. Thanks!)
Last updated: Oct 13 2024 at 01:02 UTC