Comment on Dafny is a verification-aware programming languageparentComments−IshKebab2yIt'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.−naasking2yWould that call for replacing that function with some kind of inductive abstraction to help it see that it generalizes to N byte numbers?
Comments
It'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.
Would that call for replacing that function with some kind of inductive abstraction to help it see that it generalizes to N byte numbers?