3 ms·
> I kept hitting cases where things wouldn't verify, and the reason is due to something deep in the implementation that really only the authors would know about
by naasking 3y ago
> I kept hitting cases where things wouldn't verify, and the reason is due to something deep in the implementation that really only the authors would know about.
Can you recall a specific example? I'm not only curious how this comes about, but how Dafny expects you to resolve it. You must have to declare some kind of invariant for that property somewhere. This was the case when I played with C#'s code contracts, and sometimes this was challenging to ensure.
- IshKebab 3y agoIt's been a while but there was something about Dafny only loop unrolling or maybe inlining functions a certain number of times which meant my proof worked for like 1 and 2 byte numbers but not 3 or more.
- naasking 3y agoWould that call for replacing that function with some kind of inductive abstraction to help it see that it generalizes to N byte numbers?