pschanely

import re
from typing import Tuple

def parse_int_pair(s: str) -> Tuple[int, int]:
    '''
    raises: ValueError
    
    # Wrong, but Crosshair can't generate the input it needs to detect it:
    post: len(__return__) == 3
    '''

pschanely

from typing import TypeVar, NewType, List, Optional, Generic

T = TypeVar('T')
def not_empty(arr: List[T]) -> bool:
    return len(arr) > 0

def add_seven(l: List[int]) -> List[int]:
    ''' post: not_empty(__return__) '''
    return l + [7]

pschanely

class HasConsistentHash:
    '''
    A mixin to enforce that classes have hash methods that are consistent
    with thier equality checks.
    '''
    def __eq__(self, other: object) -> bool:
        '''
        post: implies(__return__, hash(self) == hash(other))
        '''
        raise NotImplementedError

pschanely

def make_bigger(n: int) -> int:
 '''
 post: __return__ > 1
 '''
 return (n+333333)*(n+333) +1
 

pschanely

def make_bigger(n: int) -> int:
  '''
  post: __return__ != 0
  '''
  return 2 * n + 10

pschanely

from typing import List

def average(numbers: List[float]) -> float:
    '''
    pre: len(numbers) >= 0
    post: min(numbers) <= __return__ <= max(numbers)
    '''
    return sum(numbers) / len(numbers)

pschanely

def make_bigger(s: str) -> str:
 '''
 post: __return__ != 'FOO'
 '''
 return s.upper()
 

pschanely

class HasConsistentHash:
    '''
    A mixin to enforce that classes have hash methods that are consistent
    with thier equality checks.
    '''
    def __eq__(self, other: object) -> bool:
        '''
        post: implies(__return__, hash(self) == hash(other))
        '''
        raise NotImplementedError

pschanely

import string
def caps(s: str) -> str:
  '''
  pre: len(s) > 0
  post: len(s) == len(_)
  '''
  #   post: _[0] in string.ascii_uppercase
  return s.capitalize()

pschanely

def lpad(fill: str, min_size: int, content: str) -> str:
  '''
  Let's prove(*) leftpad, in CrossHair!

  See background and other verifications here:
  
  https://github.com/hwayne/lets-prove-leftpad
  
  (*) CrossHair uses symbolic execution to effectively find counterexamples, but