A logical formula such that its validity means some aspect of program correctness.