A Boolean formula whose value is claimed to be true. The following are all examples:
4 + 5 = 9
4 is even and 5 is odd
x is even or y is odd
x − y > 15
for all relevant i, x[i] < x[i+1]
The last assertion states that the array x is sorted into ascending order, with no repeated values.
Assertions are employed extensively in proofs of program correctness, where they are used to characterize program states.