Combines features from the functional and imperative paradigms, and supports formal specification through function preconditions, postconditions, and loop invariants.