From bdcef82fd3599a2f47c573e3416fa8de56149263 Mon Sep 17 00:00:00 2001 From: Leo Lei Date: Mon, 1 Dec 2025 15:18:52 -0600 Subject: [PATCH 1/6] palindrome test case --- proofs/palindrome.dfy | 20 ++++++++++++++++++++ testcases/palindrome.dfy | 35 +++++++++++++++++++++++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 proofs/palindrome.dfy create mode 100644 testcases/palindrome.dfy diff --git a/proofs/palindrome.dfy b/proofs/palindrome.dfy new file mode 100644 index 0000000..4183ebf --- /dev/null +++ b/proofs/palindrome.dfy @@ -0,0 +1,20 @@ +// Proofs for Palindrome.dfy + +// Lemma 1: +// If a is a palindrome, then either its length is <= 1, +// or its first and last elements are equal. +lemma Palindrome_FirstLast(a: seq) + ensures IsPalindrome(a) ==> (|a| <= 1 || a[0] == a[|a| - 1]) +{ + + +} + +// Lemma 2: +// If a is a palindrome and has length > 1, then its middle part +// (drop first and last) is also a palindrome. +lemma Palindrome_Middle(a: seq) + ensures IsPalindrome(a) && |a| > 1 ==> IsPalindrome(a[1 .. |a| - 1]) +{ + +} diff --git a/testcases/palindrome.dfy b/testcases/palindrome.dfy new file mode 100644 index 0000000..43f99be --- /dev/null +++ b/testcases/palindrome.dfy @@ -0,0 +1,35 @@ +// Palindrome.dfy +// Simple palindrome tester on sequences of ints. + +// Recursive palindrome tester: +// A sequence is a palindrome if: +// - length 0 or 1: true +// - otherwise: first == last AND the middle part is a palindrome. +function {:induction false} IsPalindrome(a: seq): bool + decreases |a| +{ + if |a| <= 1 then + true + else + a[0] == a[|a| - 1] && IsPalindrome(a[1 .. |a| - 1]) +} + +// Test 1: +// If a is a palindrome, then either its length is <= 1 +// or its first and last elements are equal. +method Test_Palindrome_FirstLast(a: seq) +{ + assert IsPalindrome(a) ==> (|a| <= 1 || a[0] == a[|a| - 1]) by { + Palindrome_FirstLast(a); + } +} + +// Test 2: +// If a is a palindrome of length > 1, then its "middle" +// (drop first and last element) is also a palindrome. +method Test_Palindrome_Middle(a: seq) +{ + assert IsPalindrome(a) && |a| > 1 ==> IsPalindrome(a[1 .. |a| - 1]) by { + Palindrome_Middle(a); + } +} From a7361cd4ad0579ac104ff462674376bc1ac95692 Mon Sep 17 00:00:00 2001 From: Leo Lei Date: Mon, 1 Dec 2025 15:44:26 -0600 Subject: [PATCH 2/6] added induction false --- proofs/palindrome.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proofs/palindrome.dfy b/proofs/palindrome.dfy index 4183ebf..a250931 100644 --- a/proofs/palindrome.dfy +++ b/proofs/palindrome.dfy @@ -3,7 +3,7 @@ // Lemma 1: // If a is a palindrome, then either its length is <= 1, // or its first and last elements are equal. -lemma Palindrome_FirstLast(a: seq) +lemma {:induction false} Palindrome_FirstLast(a: seq) ensures IsPalindrome(a) ==> (|a| <= 1 || a[0] == a[|a| - 1]) { @@ -13,7 +13,7 @@ lemma Palindrome_FirstLast(a: seq) // Lemma 2: // If a is a palindrome and has length > 1, then its middle part // (drop first and last) is also a palindrome. -lemma Palindrome_Middle(a: seq) +lemma {:induction false} Palindrome_Middle(a: seq) ensures IsPalindrome(a) && |a| > 1 ==> IsPalindrome(a[1 .. |a| - 1]) { From 79bc63627b00d44408ae9dce46e454726069ff30 Mon Sep 17 00:00:00 2001 From: Leo Lei Date: Wed, 3 Dec 2025 21:49:55 -0600 Subject: [PATCH 3/6] made fixed suggestions --- testcases/palindrome.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/testcases/palindrome.dfy b/testcases/palindrome.dfy index 43f99be..5843fd7 100644 --- a/testcases/palindrome.dfy +++ b/testcases/palindrome.dfy @@ -5,7 +5,7 @@ // A sequence is a palindrome if: // - length 0 or 1: true // - otherwise: first == last AND the middle part is a palindrome. -function {:induction false} IsPalindrome(a: seq): bool +predicate {:induction false} IsPalindrome(a: seq): bool decreases |a| { if |a| <= 1 then @@ -17,7 +17,7 @@ function {:induction false} IsPalindrome(a: seq): bool // Test 1: // If a is a palindrome, then either its length is <= 1 // or its first and last elements are equal. -method Test_Palindrome_FirstLast(a: seq) +method {:induction false} Test_Palindrome_FirstLast(a: seq) { assert IsPalindrome(a) ==> (|a| <= 1 || a[0] == a[|a| - 1]) by { Palindrome_FirstLast(a); @@ -27,7 +27,7 @@ method Test_Palindrome_FirstLast(a: seq) // Test 2: // If a is a palindrome of length > 1, then its "middle" // (drop first and last element) is also a palindrome. -method Test_Palindrome_Middle(a: seq) +method {induction: false} Test_Palindrome_Middle(a: seq) { assert IsPalindrome(a) && |a| > 1 ==> IsPalindrome(a[1 .. |a| - 1]) by { Palindrome_Middle(a); From 7fe7488e2fffc46750a2613bc4a5db21bc0a913d Mon Sep 17 00:00:00 2001 From: Leo Lei Date: Wed, 3 Dec 2025 23:29:40 -0600 Subject: [PATCH 4/6] fixed typo and predicate explicit return --- testcases/palindrome.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/testcases/palindrome.dfy b/testcases/palindrome.dfy index 5843fd7..808db82 100644 --- a/testcases/palindrome.dfy +++ b/testcases/palindrome.dfy @@ -5,7 +5,7 @@ // 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): bool +predicate {:induction false} IsPalindrome(a: seq) decreases |a| { if |a| <= 1 then @@ -27,7 +27,7 @@ method {:induction false} Test_Palindrome_FirstLast(a: seq) // 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) +method {:induction false} Test_Palindrome_Middle(a: seq) { assert IsPalindrome(a) && |a| > 1 ==> IsPalindrome(a[1 .. |a| - 1]) by { Palindrome_Middle(a); From e5da15d6bc9530c2e010c3415bdc1c445630963b Mon Sep 17 00:00:00 2001 From: Leo Lei Date: Wed, 3 Dec 2025 23:57:25 -0600 Subject: [PATCH 5/6] made predicate opaque so it doesnt verify --- proofs/palindrome.dfy | 6 +++--- testcases/palindrome.dfy | 8 +++----- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/proofs/palindrome.dfy b/proofs/palindrome.dfy index a250931..d2d3835 100644 --- a/proofs/palindrome.dfy +++ b/proofs/palindrome.dfy @@ -1,13 +1,12 @@ // Proofs for Palindrome.dfy // Lemma 1: -// If a is a palindrome, then either its length is <= 1, +// If a is a palindrome, then either its length is <= 1 // or its first and last elements are equal. lemma {:induction false} Palindrome_FirstLast(a: seq) ensures IsPalindrome(a) ==> (|a| <= 1 || a[0] == a[|a| - 1]) { - } // Lemma 2: @@ -16,5 +15,6 @@ lemma {:induction false} Palindrome_FirstLast(a: seq) lemma {:induction false} Palindrome_Middle(a: seq) ensures IsPalindrome(a) && |a| > 1 ==> IsPalindrome(a[1 .. |a| - 1]) { - + } + diff --git a/testcases/palindrome.dfy b/testcases/palindrome.dfy index 808db82..82e75aa 100644 --- a/testcases/palindrome.dfy +++ b/testcases/palindrome.dfy @@ -5,13 +5,11 @@ // 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) +predicate {:induction false, :opaque} IsPalindrome(a: seq) decreases |a| { - if |a| <= 1 then - true - else - a[0] == a[|a| - 1] && IsPalindrome(a[1 .. |a| - 1]) + |a| <= 1 || + (a[0] == a[|a| - 1] && IsPalindrome(a[1 .. |a| - 1])) } // Test 1: From 461e666c6e36e03b908140905815b56058fd4220 Mon Sep 17 00:00:00 2001 From: Leo Lei Date: Thu, 4 Dec 2025 00:09:06 -0600 Subject: [PATCH 6/6] fixed without using opaque --- proofs/palindrome.dfy | 6 ++++-- testcases/palindrome.dfy | 3 ++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/proofs/palindrome.dfy b/proofs/palindrome.dfy index d2d3835..bbeea4b 100644 --- a/proofs/palindrome.dfy +++ b/proofs/palindrome.dfy @@ -6,7 +6,8 @@ lemma {:induction false} Palindrome_FirstLast(a: seq) ensures IsPalindrome(a) ==> (|a| <= 1 || a[0] == a[|a| - 1]) { - + // TODO replace this with a real proof. + assert false; } // Lemma 2: @@ -15,6 +16,7 @@ lemma {:induction false} Palindrome_FirstLast(a: seq) lemma {:induction false} Palindrome_Middle(a: seq) ensures IsPalindrome(a) && |a| > 1 ==> IsPalindrome(a[1 .. |a| - 1]) { - + // TODO replace this with a real proof. + assert false; } diff --git a/testcases/palindrome.dfy b/testcases/palindrome.dfy index 82e75aa..00ead7e 100644 --- a/testcases/palindrome.dfy +++ b/testcases/palindrome.dfy @@ -5,13 +5,14 @@ // A sequence is a palindrome if: // - length 0 or 1: true // - otherwise: first == last AND the middle part is a palindrome. -predicate {:induction false, :opaque} IsPalindrome(a: seq) +predicate {:induction false} IsPalindrome(a: seq) decreases |a| { |a| <= 1 || (a[0] == a[|a| - 1] && IsPalindrome(a[1 .. |a| - 1])) } + // Test 1: // If a is a palindrome, then either its length is <= 1 // or its first and last elements are equal.