On the Correctness of Barron and Strachey’s Cartesian Product Function
摘要
This paper shows how to verify Barron and Strachey’s Cartesian product function. Doing so is not only a useful exercise in the specification and verification of a classic functional program—but gives insight into the importance of formulating soundness and completeness as symmetrical properties.