Open
Description
Consider the following program (a solution to https://www.hackerrank.com/challenges/mini-max-sum/problem):
from typing import List, Tuple, Optional
from icontract import require, ensure
@require(lambda numbers: all(1 <= number <= 10**9 for number in numbers))
@require(lambda numbers: 2 <= len(numbers) < 1000)
@ensure(lambda numbers, result: 1 <= result[0] < sum(numbers))
@ensure(lambda numbers, result: 1 <= result[1] < sum(numbers))
@ensure(lambda result: result[0] <= result[1])
def slow_and_simple_find_min_max(numbers: List[int]) -> Tuple[int, int]:
"""
>>> slow_and_simple_find_min_max([1, 2, 3, 4, 5])
(10, 14)
"""
min_sum = None # type: Optional[int]
max_sum = None # type: Optional[int]
for i in range(len(numbers)):
a_sum = 0
for j in range(len(numbers)):
if i == j:
continue
a_sum += numbers[j]
min_sum = min(a_sum, min_sum)
max_sum = max(a_sum, max_sum)
return min_sum, max_sum
CrossHair 0.0.34 fails to figure out that putting a None in min or max is going to crash the program.
The doctest fails with an exception, as expected.
The correct program looks like this (mind the lines min_sum = ... and max_sum = ...):
from typing import List, Tuple, Optional
from icontract import require, ensure
@require(lambda numbers: all(1 <= number <= 10**9 for number in numbers))
@require(lambda numbers: 2 <= len(numbers) < 1000)
@ensure(lambda numbers, result: 1 <= result[0] < sum(numbers))
@ensure(lambda numbers, result: 1 <= result[1] < sum(numbers))
@ensure(lambda result: result[0] <= result[1])
def slow_and_simple_find_min_max(numbers: List[int]) -> Tuple[int, int]:
"""
>>> slow_and_simple_find_min_max([1, 2, 3, 4, 5])
(10, 14)
"""
min_sum = None # type: Optional[int]
max_sum = None # type: Optional[int]
for i in range(len(numbers)):
a_sum = 0
for j in range(len(numbers)):
if i == j:
continue
a_sum += numbers[j]
min_sum = min(a_sum, min_sum) if min_sum is not None else a_sum
max_sum = max(a_sum, max_sum) if max_sum is not None else a_sum
return min_sum, max_sum
I ran CrossHair 0.0.34 with:
crosshair check --analysis_kind icontract .\playground\exercise_02.py
Letting CrossHair in watch mode run longer did not help either:
crosshair watch --analysis_kind icontract .\playground\exercise_02.py
Metadata
Metadata
Assignees
Labels
No labels