Problem
Gengo has predicates on types (checked at construction), but no way to express constraints at the function boundary. Ada's with Pre => and with Post => aspects allow contracts that the type alone cannot express.
func divide(a int, b int) int
pre b != 0
post result == a div b
{
return a div b
}
Use cases
- Preconditions on inputs that the type alone cannot enforce (e.g. "second argument must not be zero", "array must be non-empty")
- Postconditions for documentation and debugging (checked in debug builds, elided in release)
- Richer error messages than a runtime panic: "precondition violated: b must not be zero"
Design questions
- Checked always, or only in a debug/assert build mode?
- Can preconditions reference multiple parameters together (cross-parameter constraints)?
- Syntax:
pre/post as keywords, or requires/ensures, or aspect-style annotations?
- Interaction with named return values: postconditions can reference named returns.
- Should violation be a panic (like
assert) or a typed error?
Needs design before implementation.
Problem
Gengo has predicates on types (checked at construction), but no way to express constraints at the function boundary. Ada's
with Pre =>andwith Post =>aspects allow contracts that the type alone cannot express.Use cases
Design questions
pre/postas keywords, orrequires/ensures, or aspect-style annotations?assert) or a typed error?Needs design before implementation.