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

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

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

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

from crosshair.z3util import z3IntVal

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

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