language · language ·
Requires, ensures, and invariants
Contracts attach executable meaning to valid inputs, promised outputs, and valid object state.
Use contracts at important boundaries where callers and maintainers need one visible definition of correctness.
Function(...) -> Type requires(condition) ensures(condition) { ... }
invariant(condition)Status: experimental
Contract pass
Use contracts at important boundaries where callers and maintainers need one visible definition of correctness.
cpu · complete-program · type checked
Increment(int value) returns int
requires(value > 0)
ensures(result == value + 1)
{
return value + 1
}
Console.Log(Text.From(Increment(4)))
project.mech
package = "tests.compiler.errorsTasksEffects.contractPass"
version = "0.1.0"
backend = "cpu-oracle"
osTarget = "windows"
archTarget = "x64"
selfContainedApp = false
Notes and source
Errors and contracts are experimental in the current conformance edition.
Keep the condition deterministic and cheap enough to be useful as evidence.
yeho/parser_declarations.cpp parseContractClauses and parseThingInvariant; conformance errors-contracts