kdrag.contrib.hoare

Hoare Logic over the python AST.

This is not an attempt to properly model the python semantics. Instead it is interpreting the python ast as a simple typed imperative language.

See: - https://en.wikipedia.org/wiki/Hoare_logic - https://softwarefoundations.cis.upenn.edu/plf-current/Hoare.html - https://en.wikipedia.org/wiki/Predicate_transformer_semantics

Functions

`wp`(stmt, P)	Weakest precondition for a statement stmt with postcondition P.
`wp_str`(s, P)	Compute the weakest precondition for a string of Python code s with postcondition P.
`wps`(stmts, P)

Classes

Hoare(pre, cmds, post, reasons)

Constructing the Hoare class is consider to be a proof.

class kdrag.contrib.hoare.Hoare(pre: BoolRef, cmds: tuple[AST, ...], post: BoolRef, reasons: list)

Bases: object

Constructing the Hoare class is consider to be a proof. It should only be constructed through it’s trusted smart constructors. It is analogous to a kd.Proof object in this sense. Using the bare constructor is analogous to asserting an axiom. Possibly useful, but at your own risk.

Alternative approaches may include: - Shallowly embedding an operational semantics inside z3 - Deeply embedding a python AST in z3 and defining an interpreter for it.

This is lighter weight than that, borrowing on useful existing facilities.

Parameters:

pre (BoolRef)
cmds (tuple[AST, ...])
post (BoolRef)
reasons (list)

__matmul__(other: Hoare) → Hoare

Compose two Hoare triples.

{P} S1 {Q1} {Q1} S2 {Q2} —————————— compose

{P} S1; S2 {Q2}

Parameters:: other (Hoare)
Return type:: Hoare

classmethod assign(cmd: Assign, P: BoolRef)

Create a Hoare triple for an assignment command.

——————- assign {P[e/x]} x = e {P}

Parameters:

cmd (Assign)
P (BoolRef)

cmds: tuple[AST, ...]

classmethod ite(cmd: If, hoare_body: Hoare, hoare_orelse: Hoare)

Parameters:

cmd (If)
hoare_body (Hoare)
hoare_orelse (Hoare)

post: BoolRef

pre: BoolRef

reasons: list

classmethod skip(P: BoolRef)

Create a Hoare triple for a skip command.

————– skip {P} skip {P}

Parameters:: P (BoolRef)

strengthen_pre(P1: BoolRef, by=[]) → Hoare

Strengthen the precondition of this Hoare triple.

{P} S {Q} P1 => P ——————– strengthen_pre

{P1} S {Q}

>>> x = smt.Int("x")
>>> Hoare.skip(x > 0).strengthen_pre(x > 1)
{x > 1} pass {x > 0}

Parameters:: P1 (BoolRef)
Return type:: Hoare

weaken_post(Q1: BoolRef, by=[]) → Hoare

Weaken the postcondition of this Hoare triple.

{P} S {Q} Q => Q1 ——————– weaken_post

{P} S {Q1}

>>> x = smt.Int("x")
>>> Hoare.skip(x > 0).weaken_post(x >= 0)
{x > 0} pass {x >= 0}

Parameters:: Q1 (BoolRef)
Return type:: Hoare

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

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:

Hoare

kdrag.contrib.hoare.wps(stmts: list[stmt], P: BoolRef) → Hoare

Parameters:

stmts (list[stmt])
P (BoolRef)

Return type:

Hoare