Add two-stack queue test #188
Conversation
Proves FIFO queue behavior using two LIFO stacks. Tests enqueue, dequeue, and transfer operations.
There was a problem hiding this comment.
Pull request overview
This PR introduces a formal verification implementation of a two-stack queue data structure in Dafny, demonstrating how FIFO queue behavior can be achieved using two LIFO stacks. The implementation includes the core data structure, operations (enqueue, dequeue, transfer), and test methods that verify correct queue semantics.
Key changes:
- Implements a
TwoStackQueuedatatype with inbox and outbox stacks - Provides enqueue, dequeue, and transfer operations with FIFO semantics
- Includes test methods that assert correctness properties using proof lemmas
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| testcases/two_stack_queue.dfy | Defines the two-stack queue data structure, operations (Enqueue, Dequeue, Transfer, Reverse), helper function QueueContents, and test methods that verify FIFO behavior |
| proofs/two_stack_queue.dfy | Contains lemma stubs (EnqueueCorrect, DequeueCorrect, TransferCorrect) that are referenced by test methods to prove correctness properties |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| @@ -0,0 +1,20 @@ | |||
| lemma {:induction false} EnqueueCorrect<T>(q: TwoStackQueue<T>, x: T) | |||
There was a problem hiding this comment.
The lemma references TwoStackQueue and QueueContents/Enqueue without importing or including the definitions from testcases/two_stack_queue.dfy. This file needs an include statement at the top to reference the main definitions.
Proves FIFO queue behavior using two LIFO stacks.
Tests enqueue, dequeue, and transfer operations.