Advertisement

Abstract

U ·(TP)2 is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He onwards. In this paper we focus on the underlying logic of the prover, emphasising those aspects that are tailored to support the style of proof so often used for UTP foundational work. These aspects include support for alphabets, type-inferencing, explicit substitution notation, and explicit meta-notation for general variable-binding lists in quantifiers. The need for these features is illustrated by a running example that develops a theory of UTP designs. We finish with a discussion of issues regarding the soundness of the proof tool, and linkages to existing “industrial strength” provers such as Isabelle, PVS or CoQ.

Keywords

Theorem Prover Sequential Composition Program Variable Proof Obligation Proof Assistant 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [But10]
    Butterfield, A.: Saoithín: A Theorem Prover for UTP. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 137–156. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  2. [But12]
    Butterfield, A.: U. (TP) 2 reference manual (draft, ongoing). Technical report, School of Computer Science and Statistics, Trinity College Dublin (July 2012), https://www.scss.tcd.ie/Andrew.Butterfield/Saoithin/
  3. [FGW10]
    Feliachi, A., Gaudel, M.-C., Wolff, B.: Unifying Theories in Isabelle/HOL. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 188–206. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  4. [FGW12]
    Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle/circus: A Process Specification and Verification Environment. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 243–260. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  5. [GS93]
    Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, Berlin (1993)Google Scholar
  6. [HH98]
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall (1998)Google Scholar
  7. [NPW02]
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHCrossRefGoogle Scholar
  8. [OCW06]
    Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying Theories in ProofPower-Z. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 123–140. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. [OCW09]
    Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Asp. Comput 21(1-2), 3–32 (2009)zbMATHCrossRefGoogle Scholar
  10. [Ros97]
    rOSCOE, A.W.: The Theory and Practise of Concurrency. Prentice-Hall, Pearson (1997); revised to 2000 and lightly revised to 2005Google Scholar
  11. [The08]
    The Coq Development Team. The coq proof assistant, reference manual, version 8.2. Technical report, INRIA, Roquencourt, France (2008)Google Scholar
  12. [Tou01]
    Tourlakis, G.: On the soundness and completeness of equational predicate logics. J. Log. Comput. 11(4), 623–653 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  13. [ZC08]
    Zeyda, F., Cavalcanti, A.: Encoding Circus Programs in ProofPower-Z. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 218–237. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Andrew Butterfield
    • 1
  1. 1.Lero@TCDTrinity College DublinIreland

Personalised recommendations