chickadee » simple-contracts » xlambda

(xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) . body)syntax
(xlambda ((r r? ...) (a a? ...) ... [as as? ...]) . body)syntax

contract guarded version of lambda, where k is the number of returned values r ..., if provided, 1 otherwise, r? ... their corresponding postconditions, a ... are fixed arguments with preconditions a? ..., as is an optional variable argument with preconditions as? ...

procedures with state change should return old versions of state variables before the state change