Conversation
laynotlee
force-pushed
the
leolei/palindromes
branch
from
916eda2 to
79bc636
Compare
|
Modified my test case according to suggestions, made a function a predicate to be more idiomatic. |
testcases/palindrome.dfy
Outdated
| // Test 2: | ||
| // If a is a palindrome of length > 1, then its "middle" | ||
| // (drop first and last element) is also a palindrome. | ||
| method {induction: false} Test_Palindrome_Middle(a: seq<int>) |
There was a problem hiding this comment.
Typo – should be {:induction false} instead of {induction: false}
testcases/palindrome.dfy
Outdated
| // A sequence is a palindrome if: | ||
| // - length 0 or 1: true | ||
| // - otherwise: first == last AND the middle part is a palindrome. | ||
| predicate {:induction false} IsPalindrome(a: seq<int>): bool |
There was a problem hiding this comment.
predicates always return a bool; dafny errors because of the explicit declaration
There was a problem hiding this comment.
Oh good catch, I saw the predicate but didn't check the explicit declaration at the end, oops.
There was a problem hiding this comment.
Didn't know that would be an error, just fixed.
|
This verifies with the lemma bodies empty... |
Okay, should be fixed now. |
There was a problem hiding this comment.
I get
testcases/palindrome.dfy(8,29): Error: invalid UnaryExpression
|
8 | predicate {:induction false, :opaque} IsPalindrome(a: seq<int>)
| ^
testcases/palindrome.dfy(8,36): Error: invalid TopDecl
|
8 | predicate {:induction false, :opaque} IsPalindrome(a: seq<int>)
| ^
when running the revised version locally on my machine.
Okay, should have workaround. |
5 participants
Two functions: first case is if palindrome length is less than or equal to 1.
Second case is use recursion to see if the middle string is also palindrome.