kdrag.contract

Module Attributes

contracts

kd.Proof): assert f not in contracts contracts[f] = proof

Functions

contract(f, args, pre, post[, by])	Register the contract for function f: for all args, pre => post.
lemmas(e)	Instantiate all contract lemmas found in
prove(thm[, by])

Classes

Contract(f, args, pre, post, proof)

class kdrag.contract.Contract(f: z3.z3.FuncDeclRef, args: list[z3.z3.ExprRef], pre: z3.z3.BoolRef, post: z3.z3.BoolRef, proof: kdrag.kernel.Proof)

Bases: object

Parameters:

• f (FuncDeclRef)

• args (list[ExprRef])

• pre (BoolRef)

• post (BoolRef)

• proof (Proof)

args: list[ExprRef]

f: FuncDeclRef

post: BoolRef

pre: BoolRef

proof: Proof

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

kdrag.contract.contracts: dict[FuncDeclRef, Contract] = {}

kd.Proof): assert f not in contracts contracts[f] = proof

Type:

def add_contract(f

Type:

smt.FuncDeclRef, proof

kdrag.contract.lemmas(e: ExprRef) → list[Proof]

Instantiate all contract lemmas found in

Parameters:

e (ExprRef)

Return type:

list[Proof]

kdrag.contract.prove(thm: BoolRef, by=[], **kwargs) → Proof

Parameters:

thm (BoolRef)

Return type:

Proof