Skip to content

Instantly share code, notes, and snippets.

View pschanely's full-sized avatar

Phillip Schanely pschanely

100 followers · 28 following
View GitHub Profile
@pschanely
pschanely / main.py
Created December 10, 2025 17:37
Shared via CrossHair Playground
def make_bigger(n: int) -> int:
'''
post: __return__ % 2 == 0
'''
sum = 0
for i in range(n):
sum += 2
return sum
@pschanely
pschanely / main.py
Created November 28, 2025 12:47
Shared via CrossHair Playground
def make_bigger(n: int) -> int:
'''
post: __return__ != 0
'''
return 2 * n + 10
@pschanely
pschanely / main.py
Created November 26, 2025 12:30
Shared via CrossHair Playground
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
pschanely / main.py
Created November 16, 2025 19:43
Shared via CrossHair Playground
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
pschanely / main.py
Created November 15, 2025 03:03
Shared via CrossHair Playground
def make_bigger(n: int) -> int:
'''
post: __return__ != 0
'''
return 2 * n + 10
@pschanely
pschanely / main.py
Created November 15, 2025 01:40
Shared via CrossHair Playground
def make_bigger(n: int) -> int:
'''
post: __return__ != 0
'''
return 2 * n + 10
@pschanely
pschanely / main.py
Created November 13, 2025 19:10
Shared via CrossHair Playground
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
pschanely / main.py
Created November 13, 2025 18:41
Shared via CrossHair Playground
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
pschanely / main.py
Created November 13, 2025 13:07
Shared via CrossHair Playground
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
pschanely / main.py
Created November 4, 2025 22:54
Shared via CrossHair Playground
def program1(a, b):
x = 0
y = 1
if a != 4:
x = 3 + y
if b == 3:
y = 2 * (a + b)
assert(y - x != 0)