Automated Theorem Prover Assisted Program Calculations

Abstract. Calculational Style of Programming, while very appealing, has several practical difficulties when done manually. Due to the large number of proofs involved, the derivations can be cumbersome and error-prone. To address these issues, we have developed automated theorem provers assisted program and formula transformation rules, which when coupled with the ability to extract context of a subformula, help in shortening and simplifying the derivations. We have implemented this approach in a Calculational Assistant for Programming from Specifi-cations (CAPS). With the help of simple examples, we show how the calculational assistant helps in taking the drudgery out of the derivation process while ensuring correctness