Vague postconditions and proving correctness of algorithms
Introduction
@@ -26,7 +26,7 @@To implement select sort from the exercises and make it as easy to read as possible, I have implemented maximum function that returns index of the biggest element from the first elements.
For the sake of time and memory complexity, I am also using itertools.islice, which makes a slice, but does not copy the elements into the memory like normal slice does.
There is also a check_loop_invariant function that will be described later.
def compare_by_value(pair):
index, value = pair
return value
def maximum(arr, n):
first_n_elements = itertools.islice(enumerate(arr), n)
index, value = max(first_n_elements, key=compare_by_value)
return index
def select_sort(arr, n):
assert n == len(arr)
check_loop_invariant(arr, n, n)
for i in reversed(range(1, n)):
j = maximum(arr, i + 1)
arr[i], arr[j] = arr[j], arr[i]
check_loop_invariant(arr, n, i)
return arr
def compare_by_value(pair):
index, value = pair
return value
def maximum(arr, n):
first_n_elements = itertools.islice(enumerate(arr), n)
index, value = max(first_n_elements, key=compare_by_value)
return index
def select_sort(arr, n):
assert n == len(arr)
check_loop_invariant(arr, n, n)
for i in reversed(range(1, n)):
j = maximum(arr, i + 1)
arr[i], arr[j] = arr[j], arr[i]
check_loop_invariant(arr, n, i)
return arr
Discussed preconditions, loop invariants and postconditions
You can safely replace A with arr or array for list.
Precondition
@@ -66,26 +66,26 @@maximum + index.
This will ensure that even if the maximum in the original array was the first element, I will always satisfy that 2nd part of the loop invariant.def broken_select_sort(arr, n):
assert n == len(arr)
if not arr:
return
max_value = max(arr)
check_loop_invariant(arr, n, n)
for i in reversed(range(n)):
arr[i] = max_value + i
check_loop_invariant(arr, n, i)
return arr
def broken_select_sort(arr, n):
assert n == len(arr)
if not arr:
return
max_value = max(arr)
check_loop_invariant(arr, n, n)
for i in reversed(range(n)):
arr[i] = max_value + i
check_loop_invariant(arr, n, i)
return arr
tip
There is also an easier way to break this, I leave that as an exercise ;)
Property-based tests for our sorts
Since we have talked a lot about proofs at the seminar, I would like to demonstrate it on the testing of the sorts. In the following text I will cover implementation of the loop invariant and both postconditions we have talked about and then test our sorts using them.
Loop invariant
To check loop invariant I have implemented this function:
-def check_loop_invariant(arr, n, i):
# A[i + 1 : n] is sorted
for x, y in zip(itertools.islice(arr, i + 1, n), itertools.islice(arr, i + 2, n)):
assert x <= y
# all elements of A[i + 1 : n] are bigger or equal to the other elements
if i + 1 >= n:
# in case there are no elements
return
# otherwise, since the "tail" is sorted, we can assume that it is enough to
# check the other elements to the smallest value of the tail
smallest = arr[i + 1]
for element in itertools.islice(arr, i + 1):
assert smallest >= element
def check_loop_invariant(arr, n, i):
# A[i + 1 : n] is sorted
for x, y in zip(itertools.islice(arr, i + 1, n), itertools.islice(arr, i + 2, n)):
assert x <= y
# all elements of A[i + 1 : n] are bigger or equal to the other elements
if i + 1 >= n:
# in case there are no elements
return
# otherwise, since the "tail" is sorted, we can assume that it is enough to
# check the other elements to the smallest value of the tail
smallest = arr[i + 1]
for element in itertools.islice(arr, i + 1):
assert smallest >= element
First part checks if the "ending" of the array is sorted.
In second part I have used a dirty trick of taking just the first element that is the smallest and compared the rest of the elements to it. Why is it enough? I leave it as an exercise ;)
Postcondition(s)
I have defined both the vague and explicit postconditions:
-def check_vague_postcondition(original_arr, arr):
if not arr:
return
# check ordering
for x, y in zip(arr, itertools.islice(arr, 1, len(arr))):
assert x <= y
def check_postcondition(original_arr, arr):
if not arr:
return
# check ordering
for x, y in zip(arr, itertools.islice(arr, 1, len(arr))):
assert x <= y
# get counts from original list
original_counts = {}
for value in original_arr:
original_counts[value] = 1 + original_counts.get(value, 0)
# get counts from resulting list
counts = {}
for value in arr:
counts[value] = 1 + counts.get(value, 0)
# if arr is permutation of original_arr then all counts must be the same
assert counts == original_counts
def check_vague_postcondition(original_arr, arr):
if not arr:
return
# check ordering
for x, y in zip(arr, itertools.islice(arr, 1, len(arr))):
assert x <= y
def check_postcondition(original_arr, arr):
if not arr:
return
# check ordering
for x, y in zip(arr, itertools.islice(arr, 1, len(arr))):
assert x <= y
# get counts from original list
original_counts = {}
for value in original_arr:
original_counts[value] = 1 + original_counts.get(value, 0)
# get counts from resulting list
counts = {}
for value in arr:
counts[value] = 1 + counts.get(value, 0)
# if arr is permutation of original_arr then all counts must be the same
assert counts == original_counts
Putting it together
Now that we have everything implement, we can move on to the implementation of the tests:
-from hypothesis import given, settings
from hypothesis.strategies import integers, lists
import pytest
@given(lists(integers()))
@settings(max_examples=1000)
@pytest.mark.parametrize(
"postcondition", [check_vague_postcondition, check_postcondition]
)
@pytest.mark.parametrize("sorting_function", [select_sort, broken_select_sort])
def test_select_sort(sorting_function, postcondition, numbers):
result = sorting_function(numbers[:], len(numbers))
postcondition(numbers, result)
from hypothesis import given, settings
from hypothesis.strategies import integers, lists
import pytest
@given(lists(integers()))
@settings(max_examples=1000)
@pytest.mark.parametrize(
"postcondition", [check_vague_postcondition, check_postcondition]
)
@pytest.mark.parametrize("sorting_function", [select_sort, broken_select_sort])
def test_select_sort(sorting_function, postcondition, numbers):
result = sorting_function(numbers[:], len(numbers))
postcondition(numbers, result)
Since it might seem a bit scary, I will disect it by parts.
-
Parameters of test function
-+def test_select_sort(sorting_function, postcondition, numbers):def test_select_sort(sorting_function, postcondition, numbers):We are given 3 parameters:
sorting_function- as the name suggests is the sorting function we test
@@ -95,7 +95,7 @@ This will ensure that even if the maximum in the original array was the first el
-
Body of the test
-+result = sorting_function(numbers[:], len(numbers))
postcondition(numbers, result)result = sorting_function(numbers[:], len(numbers))
postcondition(numbers, result)We pass to the sorting function copy of the numbers we got, this ensures that once we are checking the more strict postcondition, we can gather the necessary information even after sorting the list in-situ, i.e. we can check if the
resultis really apermutationof thenumberseven though the sorting functions has modified the passed in list.
-
1st
-parametrizefrom the bottom+@pytest.mark.parametrize("sorting_function", [select_sort, broken_select_sort])@pytest.mark.parametrize("sorting_function", [select_sort, broken_select_sort])This tells pytest, that we want to pass the values from the list to the parameter
sorting_function. In other words, this lets us use the same test function for both the correct and incorrect select sort. - @@ -120,7 +120,7 @@ This means hypothesis is randomly creating lists of integers and passing them to
Let's run the tests!
In case you want to experiment locally, you should install pytest and hypothesis from the PyPI.
% pytest -v test_sort.py
=================================== test session starts ====================================
platform linux -- Python 3.6.8, pytest-3.8.2, py-1.7.0, pluggy-0.13.1 -- /usr/bin/python3
cachedir: .pytest_cache
rootdir: /home/xfocko/git/xfocko/ib002/postcondition-ambiguity, inifile:
plugins: hypothesis-5.16.1
collected 4 items
test_sort.py::test_select_sort[select_sort-check_vague_postcondition] PASSED [ 25%]
test_sort.py::test_select_sort[select_sort-check_postcondition] PASSED [ 50%]
test_sort.py::test_select_sort[broken_select_sort-check_vague_postcondition] PASSED [ 75%]
test_sort.py::test_select_sort[broken_select_sort-check_postcondition] FAILED [100%]
========================================= FAILURES =========================================
_________________ test_select_sort[broken_select_sort-check_postcondition] _________________
sorting_function = <function broken_select_sort at 0x7fac179308c8>
postcondition = <function check_postcondition at 0x7fac1786d1e0>
@given(lists(integers()))
> @settings(max_examples=1000)
@pytest.mark.parametrize(
"postcondition", [check_vague_postcondition, check_postcondition]
)
@pytest.mark.parametrize("sorting_function", [select_sort, broken_select_sort])
def test_select_sort(sorting_function, postcondition, numbers):
test_sort.py:132:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
test_sort.py:139: in test_select_sort
postcondition(numbers, result)
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
original_arr = [0, 0], arr = [0, 1]
def check_postcondition(original_arr, arr):
if not arr:
return
# check ordering
for x, y in zip(arr, itertools.islice(arr, 1, len(arr))):
assert x <= y
# get counts from original list
original_counts = {}
for value in original_arr:
original_counts[value] = 1 + original_counts.get(value, 0)
# get counts from resulting list
counts = {}
for value in arr:
counts[value] = 1 + counts.get(value, 0)
# if arr is permutation of original_arr then all counts must be the same
> assert counts == original_counts
E assert {0: 1, 1: 1} == {0: 2}
E Differing items:
E {0: 1} != {0: 2}
E Left contains more items:
E {1: 1}
E Full diff:
E - {0: 1, 1: 1}
E + {0: 2}
test_sort.py:128: AssertionError
----------------------------------- Captured stdout call -----------------------------------
Falsifying example: test_select_sort(
sorting_function=<function test_sort.broken_select_sort>,
postcondition=<function test_sort.check_postcondition>,
numbers=[0, 0],
)
============================ 1 failed, 3 passed in 6.84 seconds ============================
% pytest -v test_sort.py
=================================== test session starts ====================================
platform linux -- Python 3.6.8, pytest-3.8.2, py-1.7.0, pluggy-0.13.1 -- /usr/bin/python3
cachedir: .pytest_cache
rootdir: /home/xfocko/git/xfocko/ib002/postcondition-ambiguity, inifile:
plugins: hypothesis-5.16.1
collected 4 items
test_sort.py::test_select_sort[select_sort-check_vague_postcondition] PASSED [ 25%]
test_sort.py::test_select_sort[select_sort-check_postcondition] PASSED [ 50%]
test_sort.py::test_select_sort[broken_select_sort-check_vague_postcondition] PASSED [ 75%]
test_sort.py::test_select_sort[broken_select_sort-check_postcondition] FAILED [100%]
========================================= FAILURES =========================================
_________________ test_select_sort[broken_select_sort-check_postcondition] _________________
sorting_function = <function broken_select_sort at 0x7fac179308c8>
postcondition = <function check_postcondition at 0x7fac1786d1e0>
@given(lists(integers()))
> @settings(max_examples=1000)
@pytest.mark.parametrize(
"postcondition", [check_vague_postcondition, check_postcondition]
)
@pytest.mark.parametrize("sorting_function", [select_sort, broken_select_sort])
def test_select_sort(sorting_function, postcondition, numbers):
test_sort.py:132:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
test_sort.py:139: in test_select_sort
postcondition(numbers, result)
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
original_arr = [0, 0], arr = [0, 1]
def check_postcondition(original_arr, arr):
if not arr:
return
# check ordering
for x, y in zip(arr, itertools.islice(arr, 1, len(arr))):
assert x <= y
# get counts from original list
original_counts = {}
for value in original_arr:
original_counts[value] = 1 + original_counts.get(value, 0)
# get counts from resulting list
counts = {}
for value in arr:
counts[value] = 1 + counts.get(value, 0)
# if arr is permutation of original_arr then all counts must be the same
> assert counts == original_counts
E assert {0: 1, 1: 1} == {0: 2}
E Differing items:
E {0: 1} != {0: 2}
E Left contains more items:
E {1: 1}
E Full diff:
E - {0: 1, 1: 1}
E + {0: 2}
test_sort.py:128: AssertionError
----------------------------------- Captured stdout call -----------------------------------
Falsifying example: test_select_sort(
sorting_function=<function test_sort.broken_select_sort>,
postcondition=<function test_sort.check_postcondition>,
numbers=[0, 0],
)
============================ 1 failed, 3 passed in 6.84 seconds ============================
We can clearly see that our broken select sort has passed the vague postcondition, but the explicit one was not satisfied.
Summary
For proving the correctness of the algorithm it is better to be explicit than prove that algorithm is correct even though it is not. Being explicit also allows you to test smaller chunks of code better.