Refinement of Specifications

A refinement $S\sqsubseteq T$ of program specifications is proof that for all programs $P$, $P\vDash S\to P\vDash T$.

This is a version of the Exponential of Presheaves.