Anonymous
6/12/2025, 6:18:08 PM
No.105572641
>>105572020
I'm having hard time to understand the relevance of this post
>>105572340
>Can't you just specify properties for each function and then prove that the code for that function meets them?
that's already how automated theorem provers like CBMC work with assumptions and assertions afaik but since it's computationally complex you're required to split up your code to more modular structures that can be verified independently
>because then the proof depends on the implementation of each object that the function interacts with
it doesnt if you do oop. every object have clearly defined interfaces and contracts, so that implementation details only matter while you're proving the invariant and postconditions for individual objects
I'm having hard time to understand the relevance of this post
>>105572340
>Can't you just specify properties for each function and then prove that the code for that function meets them?
that's already how automated theorem provers like CBMC work with assumptions and assertions afaik but since it's computationally complex you're required to split up your code to more modular structures that can be verified independently
>because then the proof depends on the implementation of each object that the function interacts with
it doesnt if you do oop. every object have clearly defined interfaces and contracts, so that implementation details only matter while you're proving the invariant and postconditions for individual objects