| # This file is part of Hypothesis, which may be found at |
| # https://github.com/HypothesisWorks/hypothesis/ |
| # |
| # Most of this work is copyright (C) 2013-2021 David R. MacIver |
| # (david@drmaciver.com), but it contains contributions by others. See |
| # CONTRIBUTING.rst for a full list of people who may hold copyright, and |
| # consult the git log if you need to determine who owns an individual |
| # contribution. |
| # |
| # This Source Code Form is subject to the terms of the Mozilla Public License, |
| # v. 2.0. If a copy of the MPL was not distributed with this file, You can |
| # obtain one at https://mozilla.org/MPL/2.0/. |
| # |
| # END HEADER |
| # |
| # SPDX-License-Identifier: MPL-2.0 |
| |
| """This file demonstrates testing a binary search. |
| |
| It's a useful example because the result of the binary search is so clearly |
| determined by the invariants it must satisfy, so we can simply test for those |
| invariants. |
| |
| It also demonstrates the useful testing technique of testing how the answer |
| should change (or not) in response to movements in the underlying data. |
| """ |
| |
| from hypothesis import given, strategies as st |
| |
| |
| def binary_search(ls, v): |
| """Take a list ls and a value v such that ls is sorted and v is comparable |
| with the elements of ls. |
| |
| Return an index i such that 0 <= i <= len(v) with the properties: |
| |
| 1. ls.insert(i, v) is sorted |
| 2. ls.insert(j, v) is not sorted for j < i |
| """ |
| # Without this check we will get an index error on the next line when the |
| # list is empty. |
| if not ls: |
| return 0 |
| |
| # Without this check we will miss the case where the insertion point should |
| # be zero: The invariant we maintain in the next section is that lo is |
| # always strictly lower than the insertion point. |
| if v <= ls[0]: |
| return 0 |
| |
| # Invariant: There is no insertion point i with i <= lo |
| lo = 0 |
| |
| # Invariant: There is an insertion point i with i <= hi |
| hi = len(ls) |
| while lo + 1 < hi: |
| mid = (lo + hi) // 2 |
| if v > ls[mid]: |
| # Inserting v anywhere below mid would result in an unsorted list |
| # because it's > the value at mid. Therefore mid is a valid new lo |
| lo = mid |
| # Uncommenting the following lines will cause this to return a valid |
| # insertion point which is not always minimal. |
| # elif v == ls[mid]: |
| # return mid |
| else: |
| # Either v == ls[mid] in which case mid is a valid insertion point |
| # or v < ls[mid], in which case all valid insertion points must be |
| # < hi. Either way, mid is a valid new hi. |
| hi = mid |
| assert lo + 1 == hi |
| # We now know that there is a valid insertion point <= hi and there is no |
| # valid insertion point < hi because hi - 1 is lo. Therefore hi is the |
| # answer we were seeking |
| return hi |
| |
| |
| def is_sorted(ls): |
| """Is this list sorted?""" |
| for i in range(len(ls) - 1): |
| if ls[i] > ls[i + 1]: |
| return False |
| return True |
| |
| |
| Values = st.integers() |
| |
| # We generate arbitrary lists and turn this into generating sorting lists |
| # by just sorting them. |
| SortedLists = st.lists(Values).map(sorted) |
| |
| # We could also do it this way, but that would be a bad idea: |
| # SortedLists = st.lists(Values).filter(is_sorted) |
| # The problem is that Hypothesis will only generate long sorted lists with very |
| # low probability, so we are much better off post-processing values into the |
| # form we want than filtering them out. |
| |
| |
| @given(ls=SortedLists, v=Values) |
| def test_insert_is_sorted(ls, v): |
| """We test the first invariant: binary_search should return an index such |
| that inserting the value provided at that index would result in a sorted |
| set.""" |
| ls.insert(binary_search(ls, v), v) |
| assert is_sorted(ls) |
| |
| |
| @given(ls=SortedLists, v=Values) |
| def test_is_minimal(ls, v): |
| """We test the second invariant: binary_search should return an index such |
| that no smaller index is a valid insertion point for v.""" |
| for i in range(binary_search(ls, v)): |
| ls2 = list(ls) |
| ls2.insert(i, v) |
| assert not is_sorted(ls2) |
| |
| |
| @given(ls=SortedLists, v=Values) |
| def test_inserts_into_same_place_twice(ls, v): |
| """In this we test a *consequence* of the second invariant: When we insert |
| a value into a list twice, the insertion point should be the same both |
| times. This is because we know that v is > the previous element and == the |
| next element. |
| |
| In theory if the former passes, this should always pass. In practice, |
| failures are detected by this test with much higher probability because it |
| deliberately puts the data into a shape that is likely to trigger a |
| failure. |
| |
| This is an instance of a good general category of test: Testing how the |
| function moves in responses to changes in the underlying data. |
| """ |
| i = binary_search(ls, v) |
| ls.insert(i, v) |
| assert binary_search(ls, v) == i |