kdrag.contrib.hoare.wp

kdrag.contrib.hoare.wp(stmt: AST, P: BoolRef) → Hoare

Weakest precondition for a statement stmt with postcondition P. The Hoare class is a declarative Proof object. wp infers a useful a useful Hoare triple for a program and postcondition.

Parameters:

• stmt (AST)

• P (BoolRef)

Return type:

Hoare