Dijkstra monad

An adaptation of predicate transformer semantics to a typed functional setting.

A predicate transformer (from postconditions to preconditions) for computations with state type and result type has type A Dijkstra monad over state type has kind It can be implemented as a pair , where is an element of the state monad and is a proof that agrees with the predicate transformer parameter ; i.e., for all propositions and states , if , then .

Definition PT (S A : Type) : Type :=
  (A * S -> Prop) -> (S -> Prop).

Definition DST {S A : Type} (wp : PT S A) : Type :=
  exists (u : S -> A * S), forall (P : A * S -> Prop) (s : S), P (u s) -> wp P s.