Weakest Preconditions · Quantum PL Wiki

A weakest-precondition transformer computes an input predicate from a desired output predicate. Let $\mathcal E=\llbracket C\rrbracket$ be a completely positive, trace-nonincreasing map between finite-dimensional state spaces, and let $Q$ be an output effect. The trace adjoint $\mathcal E^*$ is characterized by

\mathrm{tr}(\mathcal E^*(Q)\rho) =\mathrm{tr}(Q\mathcal E(\rho)).

This relation turns the forward state transformation of denotational semantics into backward reasoning about observations.

Total and partial correctness

For total correctness, the weakest precondition is

\mathrm{wp}_C(Q)=\mathcal E^*(Q).

For partial correctness, where missing output trace represents nontermination, the weakest liberal precondition is

\mathrm{wlp}_C(Q)=\mathcal E^*(Q)+I-\mathcal E^*(I).

The identities inside and outside $\mathcal E^*$ act on the output and input spaces respectively. Trace nonincrease ensures $\mathcal E^*(I)\preceq I$ , so both transformers return effects. If the map preserves trace, $\mathcal E^*(I)=I$ and the two transformers agree.

Under the quantitative convention used in quantum Hoare logic, a valid total triple satisfies $P\preceq\mathrm{wp}_C(Q)$ ; a valid partial triple satisfies $P\preceq\mathrm{wlp}_C(Q)$ . Here $A\preceq B$ means $B-A$ is positive semidefinite. Consequently, the conventionally named weakest precondition is the greatest admissible precondition effect in this operator order; the term should not be interpreted through an unstated Boolean implication order.

Examples: gates, measurement, and sequencing

For a unitary $U$ , $\mathrm{wp}_U(Q)=U^\dagger QU$ . With $U=X$ and $Q=\lvert1\rangle\langle1\rvert$ , the result is $\lvert0\rangle\langle0\rvert$ .

If a measurement discards its outcome, its transformer is

\mathrm{wp}_{\mathrm{meas}}(Q)=\sum_m M_m^\dagger QM_m.

Computational-basis measurement therefore transforms the postcondition $Q=\lvert+\rangle\langle+\rvert$ into $I/2$ : after dephasing, the probability of a subsequent $+$ outcome is one half for every normalized input.

For C1; C2, backward calculation reverses execution order:

\mathrm{wp}_{C_1;C_2}(Q) =\mathrm{wp}_{C_1}(\mathrm{wp}_{C_2}(Q)).

A never-terminating program has $\mathrm{wp}(Q)=0$ but $\mathrm{wlp}(Q)=I$ , demonstrating the role of liberal correctness.

Limitations

Retained measurement results and classical control require outcome-dependent predicates or an explicit classical-quantum state space. Loops generally need fixed-point reasoning; a closed expression need not be available. Numerical matrix comparisons require justified error bounds, especially near zero eigenvalues. This introductory calculation method does not automatically generate invariants or provide a machine-checked proof.

References

Ellie D'Hondt and Prakash Panangaden. Quantum Weakest Preconditions. Mathematical Structures in Computer Science (2006). arXiv:quant-ph/0501157.
Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems 33(6), 1-49 (2011). DOI: 10.1145/2049706.2049708.