Cure
Verification-First Programming
Verification-First Programming
Function-Level Guards Example Demonstrates guards on function definitions in Cure
# Function-Level Guards Example
# Demonstrates guards on function definitions in Cure
module FunctionGuards do
export [main/0]
import Std.Io [println/1]
# === SINGLE-CLAUSE FUNCTION GUARDS ===
# Simple guard on function parameter
def is_positive(x: Int): Bool when x > 0 = true
def is_positive(x: Int): Bool when x <= 0 = false
# Guard with multiple conditions
def in_range(x: Int, min: Int, max: Int): Bool
when x >= min and x <= max
do
true
end
def in_range(x: Int, _min: Int, _max: Int): Bool = false
# === MULTI-CLAUSE FUNCTIONS WITH GUARDS ===
# Absolute value using guards
def abs(x: Int): Int when x >= 0 = x
def abs(x: Int): Int when x < 0 = -x
# Factorial with guard-based recursion
def factorial(n: Int): Int when n == 0 = 1
def factorial(n: Int): Int when n > 0 = n * factorial(n - 1)
# Sign function
def sign(x: Int): Int when x > 0 = 1
def sign(x: Int): Int when x == 0 = 0
def sign(x: Int): Int when x < 0 = -1
# === GUARDS WITH TYPE CONSTRAINTS ===
# Safe division requiring non-zero divisor
def safe_div(numerator: Int, divisor: Int): Int
when divisor != 0
do
numerator / divisor
end
# Guard ensuring valid array index
def get_element(list: List(Int), index: Int): Option(Int)
when index >= 0 and index < length(list)
do
Some(nth(list, index))
end
def get_element(_list: List(Int), _index: Int): Option(Int) = None
# === GUARDS WITH ARITHMETIC ===
# Check if number is even (using modulo in guard)
def is_even(n: Int): Bool when n % 2 == 0 = true
def is_even(_n: Int): Bool = false
# FizzBuzz using guards
def fizzbuzz(n: Int): String when n % 15 == 0 = "FizzBuzz"
def fizzbuzz(n: Int): String when n % 3 == 0 = "Fizz"
def fizzbuzz(n: Int): String when n % 5 == 0 = "Buzz"
def fizzbuzz(n: Int): String = show(n)
# === GUARDS WITH COMPLEX EXPRESSIONS ===
# Classify temperature with guard ranges
def classify_temp(celsius: Float): String
when celsius < -273.15
do
"Invalid (below absolute zero)"
end
def classify_temp(celsius: Float): String
when celsius < 0.0
do
"Freezing"
end
def classify_temp(celsius: Float): String
when celsius >= 0.0 and celsius < 25.0
do
"Cool"
end
def classify_temp(celsius: Float): String
when celsius >= 25.0 and celsius < 35.0
do
"Warm"
end
def classify_temp(_celsius: Float): String = "Hot"
# === GUARDS WITH RECORD PATTERNS ===
record Point do
x: Float
y: Float
end
# Check if point is at origin
def at_origin(p: Point): Bool
when p.x == 0.0 and p.y == 0.0
do
true
end
def at_origin(_p: Point): Bool = false
# === GUARDS FOR PRECONDITIONS ===
# Square root requiring non-negative input
def safe_sqrt(x: Float): Float
when x >= 0.0
do
sqrt(x)
end
# Logarithm requiring positive input
def safe_log(x: Float): Float
when x > 0.0
do
log(x)
end
# === RECURSIVE FUNCTIONS WITH GUARDS ===
# Sum of list using guards for base case
def sum_list(list: List(Int)): Int
when is_empty(list)
do
0
end
def sum_list(list: List(Int)): Int =
head(list) + sum_list(tail(list))
# Find maximum in list
def max_list(list: List(Int)): Option(Int)
when is_empty(list)
do
None
end
def max_list(list: List(Int)): Option(Int)
when length(list) == 1
do
Some(head(list))
end
def max_list(list: List(Int)): Option(Int) =
let first = head(list)
let rest_max = max_list(tail(list))
match rest_max do
Some(m) when first > m -> Some(first)
Some(m) -> Some(m)
None -> Some(first)
end
# === DEMONSTRATION FUNCTION ===
def main(): Int =
println("=== Function Guards Demo ===\n")
println("--- Single Positive Test ---")
println(is_positive(5)) # true
println(is_positive(-3)) # false
println("\n--- Range Test ---")
println(in_range(5, 0, 10)) # true
println(in_range(15, 0, 10)) # false
println("\n--- Absolute Value ---")
println(abs(5)) # 5
println(abs(-5)) # 5
println("\n--- Factorial ---")
println(factorial(0)) # 1
println(factorial(5)) # 120
println("\n--- Sign Function ---")
println(sign(10)) # 1
println(sign(0)) # 0
println(sign(-10)) # -1
println("\n--- Safe Division ---")
println(safe_div(10, 2)) # 5
# println(safe_div(10, 0)) # Would fail guard
println("\n--- FizzBuzz ---")
println(fizzbuzz(15)) # "FizzBuzz"
println(fizzbuzz(9)) # "Fizz"
println(fizzbuzz(10)) # "Buzz"
println(fizzbuzz(7)) # "7"
println("\n--- Temperature Classification ---")
println(classify_temp(-10.0)) # "Freezing"
println(classify_temp(20.0)) # "Cool"
println(classify_temp(30.0)) # "Warm"
println(classify_temp(40.0)) # "Hot"
println("\n--- Recursive Sum ---")
println(sum_list([1, 2, 3, 4, 5])) # 15
println("\nAll tests completed!")
0
end