Title: Data abstraction and the correctness of modular programming