examples.py

from typing import Type

# errors on: line 2, 4
# pre True
# post res != x
def some(x: int) -> int:
  return x

# pre True
# post res == x * x
def cube(x: int) -> int:
  return x * x * x

# pre n == 5
# post res == 5 * 4
def factorial(n: int) -> int:
  if n <= 1:
    return 1 
  else:
    return n * factorial(n - 1)


# correctly errors on (5, 14)
def loop_iter(n: int) -> int:
  i: int = 1
  a: int = 1
  # invariant 0 < i
  # invariant i <= n + 1
  # invariant a > 0
  while i < n + 1: 
    a = i * a
    i = i + 1
  
  return a

# correctly errors on (1, 80),(6, 7)
# post (res == a or res == b) and (a >= b ==> res == a) and (a <= b ==> res != b)
def max(a: int, b: int) -> int:
  if a > b:
    return a
  else:
    return b

# post res == n + n
def double(n: int) -> int:
  return n * 2

# decreases n
# pre n >= 0
# post res == n + 1
def increment(n: int) -> int:
  if n == 0:
    return 1 
  elif n % 2 == 1:
    return 2 * increment(n / 2)
  else:
    return n + 1

# pre n == 6
# post res == 8
def fib(n: int) -> int:
  if n == 0:
    return 0
  elif n == 1:
    return 1
  else:
    return fib(n - 1) + fib(n - 2)

# pre x == 1 and y == 2
# post res == 4
def ackermann(x: int, y: int) -> int:
  if y == 0:
    return 0
  elif x == 0:
    return 2 * y
  elif y == 1:
    return 2
  else:
    return ackermann(x - 1, ackermann(x, y - 1))

# correctly returns error on (7, 11), (2, 7)
# pre n == 3
# post res == b * b * b
def expt(b: int, n: int) -> int:
  if n == 0:
    return 1
  else:
    return b * expt(b, n - 1)

# correctly returns error on (7, 7), (2, 12) 
# pre b >= 0
# post res == a + b
def times(a: int, b: int) -> int:
  if b == 0:
    return 0
  else:
    return a + times(a, b - 1)

# def gcd(a: int, b: int) -> int:
#     if b == 0:
#         return a
#     else:
#         return gcd(b, a % b)

# correctly errors on (8, 11),(4, 23),(10, 13),(5, 24)
# decreases b - a
# pre a > 0
# pre a <= b
# post a == b ==> res == a + b
# post a != b ==> (res == a + b)
def sum_ints(a: int, b: int) -> int:
  if a == b:
    return a
  else:
    return 1 + sum_ints(a + 1, b)

# post res == a * b + x * y
def linear_combination(a: float, b: float, x: float, y: float) -> float:
  return a * x + b * y

# function call in loop specification
# post res == x     
def f(x: int) -> int:
  return x

i = 10
# invariant 0 <= i and i <= 10
# invariant i == f(i)
while 0 < i:
  i = i - 1
  
  
  
  
# type aliasing example
ConnectionOptions = dict[str, str]
Address = tuple[int, int]
Server = tuple[Address, Address]          
def broadcast_message(message: str, servers: list[Server]) -> None:
  pass
    
    
# ternary operator example
a = 2 if 4 % 2 == 0 else 3 if 10 > 20 else 4 if 1 + 1 != 2 else 5

# generics example
from typing import TypeVar

T = TypeVar("T")
S = T

# reads l
# pre len(l) > 0
# post res == l[0]
def first(l: list[S]) -> S:    
  return l[0]


# for to while loop conversion example
def add() -> int:
  a: list[tuple[int, int]] = [(1,2), (3,4)] 
  sum: int = 0
  for x in a:
    sum = sum + x[0] + x[1]
  
  print(sum)
  return sum

# function call in method spec example
# post res == (x % 2 == 0)
def even(x: int) -> bool:
  return x % 2 == 0

# post res == even(x)    
def evenM(x: int) -> bool: 
  return even(x)


# function as argument example
from typing import Callable
# post res == n + 1 
def increment(n: int) -> int:
  return (n + 1)

# post res == f(x)  
def apply(f: Callable[[int], int], x: int) -> int:
  return f(x)

i = apply(increment, 3)
assert i == 4

l = lambda x : x + 1
i2 = apply(l, 3)     
assert i2 == i

# find example
# post 0 <= res ==> res < len(a) and a[res] == key
# post res == -1 ==> forall k :: 0 <= k and k < len(a) ==> a[k] != key
def find(a: list[int], key: int) -> int:
  index = 0
  # invariant 0 <= index and index <= len(a)
  # invariant forall k :: 0 <= k and k < index ==> a[k] != key
  while index < len(a):
    if a[index] == key:
      return index
    
    index += 1
  
  return -1

# higher order example
a = [-2, 0, 1, 2]    
alwaysPositive = lambda x: x > 0
p = filter(alwaysPositive, a)
assert 1 in a and 1 in p
assert 2 in a and 2 in p
assert False

# binary search example
# reads l
def sorted(l: list[int]) -> bool:
  forall j, k :: 0 <= j and j < k and k < len(l) ==> l[j] <= l[k]

# pre sorted(l)
# post res >= 0 ==> res < len(l) and l[res] == key
# post res < 0 ==> forall k :: 0 <= k and k < len(l) ==> l[k] != key
def binarysearch(l: list[int], key: int) -> int:
  low = 0
  high = len(l)
  # invariant 0 <= low and low <= high and high <= len(l)
  # invariant forall i :: 0 <= i and i < len(l) and not (low <= i and i < high) ==> l[i] != key
  while low < high:
    mid = (low + high) / 2
    if key < l[mid]:
      high = mid
    elif key > l[mid]:
      low = mid + 1
    else:
      return mid
  
  return -1

l = [1, 2, 3, 4, 5]
ans = binarysearch(l, 4)
assert l[3] == 4
assert ans == 3
non = binarysearch(l, 6)
assert non < 0


# modification example
# modifies l         
def add(l: list[int]) -> None:
  idx = len(l)   
  l.append(10)
  assert l[idx] == 10
 
# new list example
# post fresh(res)   
def lst() -> list[int]:
  return []

# list lower, upper example
b = [1, 2, 3, 4, 5][1:3]    
assert len(b) == 2
assert b[0] == 2
assert b[1] == 3
assert b[1] == 4 # correctly errors on (5, 7)

# list lower range example
b = [1, 2, 3][0:]    
assert len(b) == 3

# list higher range example
b = [1, 2, 3][:1]    
assert len(b) == 1
assert b[0] == 1

# list no range example
b = [1, 2, 3][:]    
assert len(b) == 3
assert b[0] == 1
assert b[1] == 2
assert b[2] == 3

# lambda with type example
from typing import Callable
def line(slope : float, b : float) -> Callable[[float], float]:
  return lambda x: slope*x + b

# ensures forall i :: 0 <= i and i < res1 ==> s[i] <= x
def place(x: int, s: list[int]) -> int:
  output = 0
  # invariant 0 <= output and output <= len(s)
  # invariant forall j :: 0 <= j and j < output ==> s[j] <= x
  while output < len(s):
    if x > s[output]:
      output += 1
    else:
      break
  
  return output