kdrag.contract.contract

kdrag.contract.contract(f: FuncDeclRef, args: list[ExprRef], pre, post, by=None, **kwargs) → Proof

Register the contract for function f: for all args, pre => post.

>>> x = smt.Int("x")
>>> foo = kd.define("foo4392", [x], x + 1)
>>> c = contract(foo, [x], x > 0, foo(x) > 0, by=[foo.defn])
>>> c
|= ForAll(x, Implies(x > 0, foo4392(x) > 0))
>>> c.thm.pattern(0)
foo4392(Var(0))
>>> prove(foo(5) > 0)
|= foo4392(5) > 0
>>> prove(foo(5) > 5)
Traceback (most recent call last):
    ...
LemmaError: ...

Parameters:

• f (FuncDeclRef)

• args (list[ExprRef])

Return type:

Proof