Add BinSearch test case

[bell-boy]

Title

[Copilot]

Pull request overview

This PR adds a new binary search test case to the Dafny verification suite, consisting of an implementation and its corresponding proof structure.

Key Changes

• Adds binsearch function implementing binary search on sorted integer sequences
• Adds binsearchTest method to verify the function's correctness properties
• Adds proof lemma binsearchProof to support the verification

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.

File	Description
testcases/binsearch.dfy	Implements the binary search function and test method with preconditions ensuring sorted sequences
proofs/binsearch.dfy	Provides proof lemma structure with ensures clauses for binsearch correctness properties

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The comment refers to "bello.dfy" but this file contains proofs for "binsearch.dfy". The comment should be updated to reflect the correct filename.

Suggested change

	// Proofs for bello.dfy
	// Proofs for binsearch.dfy

[amrina18]

There is already a private test case for binary search (008).
Also, the private one is more comprehensive. It has the case of the item not being in the list and checks that the index found is correct for a specific item.