Pre-conditions and post-conditions for specify logical formula; this is the basis of verification systems.