Preliminary steps towards a theory, framework and process for proving that contract-equipped classes satisfy their contracts, including when the run-time structure involves pointers; and its application to correctness proofs of routines from a LINKED_LIST class, such as element removal and list reversal.
展开▼
