Predicate Logic
for
Specifying Programs
and
Proving their Correctness