Design Choices In Specification Languages And Verification Systems
John Rushby · 2005
We describe some of the design choices that should be considered in the development and application of specification languages and verification systems. A principal issue is the need to reconcile the desire for expressiveness in the specification language with the ability to provide effective mechanical support. We argue that this reconciliation is assisted by a novel approach to specification language design that requires theorem proving to be used during typechecking.