pschanely

from dataclasses import dataclass

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))

pschanely

def make_bigger(n: int) -> int:
  '''
  post: __return__ % 2 == 0
  '''
  sum = 0
  for i in range(n):
      sum += 2
      
  return sum

pschanely

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

pschanely

import dataclasses
from typing import List

@dataclasses.dataclass
class AverageableQueue:
    '''
    A queue of numbers with a O(1) average() operation.
    inv: self._total == sum(self._values)
    '''
    _values: List[int]

pschanely

import dataclasses
from typing import List

@dataclasses.dataclass
class AverageableQueue:
    '''
    A queue of numbers with a O(1) average() operation.
    inv: self._total == sum(self._values)
    '''
    _values: List[int]

pschanely

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

pschanely

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

pschanely

import dataclasses
from typing import List

@dataclasses.dataclass
class AverageableQueue:
    '''
    A queue of numbers with a O(1) average() operation.
    inv: self._total == sum(self._values)
    '''
    _values: List[int]

pschanely

import re

from crosshair import NoTracing
from crosshair.statespace import context_statespace

_TWO_DIGITS_REGEX = re.compile("[1-9][0-9]")
def top(ipstr: str) -> bool:
    """
    This is an example of dumping the solver state after running some python
    code.

pschanely

import re
from typing import Optional

def parse_year(yearstring: str) -> Optional[int]:
    '''
    Something is wrong with this year parser! Can you guess what it is?
    
    post: __return__ is None or 1000 <= __return__ <= 9999
    '''
    return int(yearstring) if re.match('[1-9][0-9][0-9][0-9]', yearstring) else None