kdrag.contrib.hoare.wp_str

kdrag.contrib.hoare.wp_str(s: str, P: BoolRef) → Hoare

Compute the weakest precondition for a string of Python code s with postcondition P.

>>> x,y,z = smt.Ints("x y z")
>>> wp_str("x = 3; y = x + 2; z = y + 1", y > 0)
{3 + 2 > 0} x = 3; y = x + 2; z = y + 1 {y > 0}

Parameters:

Return type:

Hoare