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:
s (str)
P (BoolRef)
- Return type: