The continuous need for more ambitious, more complex, and more dependable software systems demands mechanisms to modularize such systems and reason about their correctness. The reasoning process is affected by the programming ...