Stream: Miscellaneous

Topic: Project Euler Problem 3


view this post on Zulip Lessness (Mar 14 2023 at 19:58):

I want to make C program that solves the 3rd problem of Project Euler (find the largest prime divisor of given number) and then formally verify/prove its correctness using VST.

The current state of the C program can be found here: https://github.com/LessnessRandomness/PE/blob/main/EulerProject3.c
(I took the code of Altinak at codereview.stackexchange.com)

I don't like the fact that the program uses global variable "highest" because I worry that it makes formal verification harder... Is it correct? Or am I wrong?
If I'm correct then how can I rewrite this little program in some better way to avoid difficulties caused by global variable?

Thank you!

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 23:38):

I haven't used VST specifically, but I've used other separation logics. You could make highest local to find, and have it pass &highest to factorize; or you could try to pass highest as an input, and have find return a struct as an output. But I don't know if VST supports the last option, and I wouldn't expect the first two to be very different, since VST is a separation logic and manipulating mutable state is well-supported; you should probably try writing specs for the existing code before choosing to refactor things.


Last updated: Mar 28 2024 at 22:01 UTC