Realization and Extension of Abstract Operation Contracts for Program Logic

Maria Pelevina

For engineering software with formal correctness proofs it is crucial that proofs can be efficiently reused in case the software or its specification is changed. Unfortunately, in…