Automatic Predicate Testing in Formal Certification

You’ve only Proven What You’ve Said, Not What You Meant!
  • Franck SlamaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9762)


The use of formal methods and proof assistants helps to increase the confidence in critical software. However, a formal proof is only a guarantee relative to a formal specification, and not necessary about the real requirements. There is always a jump when going from an informal specification to a formal specification expressed in a logical theory. Thus, proving the correctness of a piece of software always makes the implicit assumption that there is adequacy between the formalised specification –written with logical statements and predicates– and the real requirements –often written in English–. Unfortunately, a huge part of the complexity lies precisely in the specification itself, and it is far from obvious that the formal specification says exactly and completely what it should say. Why should we trust more these predicates than the code that we’ve first refused to trust blindly, leading to these proofs? We show in this paper that the proving activity has not replaced the testing activity but has only changed the object which requires to be tested. Instead of testing code, we now need to test predicates. We present recent ideas about how to conduct these tests inside the proof assistant on a few examples, and how to automate them as far as possible.


Formal certification Predicate testing Proof assistant 


  1. 1.
    Abrial, J., et al.: The B-method. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398–405. Springer, Heidelberg (1991). 10.1007/BFb0020001 CrossRefGoogle Scholar
  2. 2.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development- Coq’Art. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). CrossRefzbMATHGoogle Scholar
  3. 3.
    Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23, 552–593 (2013). MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Delahaye, D.: A proof dedicated meta-language. Electr. Notes Theor. Comput. Sci. 70(2), 96–109 (2002). CrossRefzbMATHGoogle Scholar
  5. 5.
    DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Commun. ACM 22(5), 271–280 (1979). CrossRefGoogle Scholar
  6. 6.
    Slama, F., Brady, E.: Automatically proving equivalence by type-safe reflection (draft under consideration). J. Funct. Program. (2016).
  7. 7.
    Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005). summary?doi= CrossRefGoogle Scholar
  8. 8.
    Krebbers, R., Leroy, X., Wiedijk, F.: Formal C semantics: CompCert and the C standard. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 543–548. Springer, Heidelberg (2014). Google Scholar
  9. 9.
    Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009). CrossRefGoogle Scholar
  10. 10.
    Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, pp. 87–100, 25–27 September 2013.

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.University of St AndrewsScotlandUK

Personalised recommendations