Building program construction and verification tools from algebraic principles

详细信息    查看全文

• 作者：Alasdair Armstrong ; Victor B. F. Gomes ; Georg Struth
• 关键词：Program construction ; Program verification ; Semantics of imperative programs ; Algebras of programs ; Formalised mathematics ; Interactive theorem proving ; Automated theorem proving
• 刊名：Formal Aspects of Computing
• 出版年：2016
• 出版时间：April 2016
• 年：2016
• 卷：28
• 期：2
• 页码：265-293
• 全文大小：856 KB
• 参考文献：Aar92.Aarts CJ (1992) Galois connections presented calculationally
  AdBO09.Apt KR, de Boer FS, Olderog E-R (2009) Verification of sequential and concurrent programs. Springer
  AGS14a.Armstrong A, Gomes VBF, Struth G (2014) Algebraic principles for rely-guarantee style concurrency verification tools. In: Jones CB, Pihlajasaari P, Sun J (eds) FM 2014. LNCS, vol 8442. Springer, pp 78–93
  AGS14b.Armstrong A, Gomes VBF, Struth G (2014) Algebras for program correctness in Isabelle/HOL. In: Höfner P et~al (eds) RAMiCS 2014.LNCS, vol 8428. Springer, pp 49–64
  AGS14c.Armstrong A, Gomes VBF, Struth G (2014) Kleene algebras with tests and demonic refinement algebras. Archive of Formal Proofs
  AGS14d.Armstrong A, Gomes VBF, Struth G (2014) Lightweight program construction and verification tools in Isabelle/HOL. In: Giannakopoulou D, Salaün G (eds) SEFM 2014, LNCS. Springer, pp 5–19
  AK01.Angus A, Kozen D (2001) Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Cornell University
  AS12.Armstrong A, Struth G (2012) Automated reasoning in higher-order regular algebra. In: Griffin T, Kahl W (eds) RAMiCs 2012. LNCS, vol 7560. Springer
  ASW13a.Armstrong A, Struth G, Weber T (2013) Kleene algebra. Archive of Formal Proofs
  ASW13b.Armstrong A, Struth G, Weber T (2013) Program analysis and verification based on Kleene algebra in Isabelle/HOL. In: Blazy S, Paulin-Mohring C, Pichardie D (eds) ITP 2013. LNCS, vol 7998. Springer, pp 197–212
  ASW14.Armstrong A, Struth G, Weber T (2014) Programming and automating mathematics in the Tarski-Kleene hierarchy. J Log Algebr Methods Programm 83(2): 87–102MathSciNet CrossRef MATH
  BKH+08.Bulwahn L, Krauss A, Haftmann F, Erkök L, Matthews J (2008) Imperative functional programming with Isabelle/HOL. In: Aït Mohamed O, Muñoz CA, Tahar S (eds) TPHOLs 2008. LNCS, vol 5170. Springer, pp 134–149
  BP10.Braibant T, Pous D (2010) An efficient Coq tactic for deciding Kleene algebras. In K. Kaufmann and L. C. Paulson, editors, ITP 2010, volume 6172 of LNCS, pages 163–178. Springer
  CSW03.Cavalcanti A, Sampaio A, Woodcock J (2003) A refinement strategy for Circus. Formal Aspects Comput 15(2-3): 146–181CrossRef MATH
  DGS15.Dongol B, Gomes VBF, Struth G (2015) A program construction and verification tool for separation logic. In: Hinze R, Voigtländer J (eds) MPC 2015. LNCS, vol 9129. Springer, pp 137–158
  DS11.Desharnais J, Struth G (2011) Internal axioms for domain semirings. Sci Comput Program 76(3): 181–203MathSciNet CrossRef MATH
  FP13.Filliâtre J-C, Paskevich A (2013) Why3—where programs meet provers. In: Felleisen M, Gardner P (eds) ESOP 201. LNCS, vol 7792. Springer, pp 125–128
  HKKN13.Haftmann F, Krauss A, Kuncar O, Nipkow T (2013) Data refinement in Isabelle/HOL. In: Blazy S, Paulin-Mohring C, Pichardie D (eds) ITP 2013. LNCS, vol 7998. Springer, pp 100–115
  HS07.Höfner P, Struth G (2007) Automated reasoning in Kleene algebra. In: Pfenning F (ed) CADE-21. LNCS, vol 4603. Springer, pp 279–294
  Kle99.Kleymann T (1999) Hoare logic and auxiliary variables. Formal Aspect Comput 11(5): 541–566CrossRef MATH
  KN12.Krauss A, Nipkow T (2012) Proof pearl: regular expression equivalence and relation algebra. J Autom Reason 49(1): 95–106MathSciNet CrossRef MATH
  Koz97.Kozen D (1997) Kleene algebra with tests. ACM TOPLAS 19(3): 427–443MathSciNet CrossRef MATH
  Koz00.Kozen D (2000) On Hoare logic and Kleene algebra with tests. ACM TOCL 1(1): 60–76MathSciNet CrossRef
  Koz03.Kozen D (2003) Kleene algebras with tests and the static analysis of programs. Technical Report TR2003-1915, Cornell University
  KP00.Kozen D, Patron M-C (2000) Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd JW et al (eds) CL 2000. LNAI, vol 1861. Springer, pp 568–582
  KS97.Kozen D, Smith F (1997) Kleene algebra with tests: completeness and decidability. In: van Dalen D, Bezem M (eds) CSL’96. LNCS, vol 1258. Springer, pp 244–259
  Lei10.Leino RKM (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EMC, Voronkov A (eds) LPAR-16, LNCS, vol 6355. Springer, pp 348–370
  MFP91.Meijer E, Fokkinga M, Paterson R (1991) Functional programming with bananas, lenses, envelopes and barbed wire. In: Hughes J (ed) 5th ACM Conf. Functional Programming Languages and Computer Architecture. LNCS, vol 523. Springer, pp 124–144
  Mor94.Morgan C (1994) Programming from specifications, 2nd edn. Prentice Hall
  MS06a.Möller B, Struth G (2006) Algebras of modal operators and partial correctness. Theor Comput Sci 351(2): 221–239MathSciNet CrossRef MATH
  MS06b.Möller B, Struth G (2006) wp is wlp. In: MacCaull W, Winter M, Düntsch I (eds) RelMiCS 2005. LNCS, vol 3929. Springer, pp 200–211
  Nip98.Nipkow T (1998) Winskel is (almost) right: towards a mechanized semantics. Formal Aspects Comput 10(2): 171–186CrossRef MATH
  Nip02.Nipkow T (2002) Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield JC (ed) CSL 2002. LNCS, vol 2471. Springer, pp 103–119
  NMB08.Nanevski A, Morrisett JG, Birkedal L (2008) Hoare type theory, polymorphism and separation. J Funct Program 18(5-6): 865–911MathSciNet CrossRef MATH
  NPW02.Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic. LNCS, vol 2283. Springer
  Pou13.Pous D (2013) Kleene algebra with tests and Coq tools for while programs. In: Blazy S, Paulin-Mohring C, Pichardie D (eds) ITP. LNCS, vol 7998. Springer, pp 180–196
  Sch08.Schirmer N (2008) A sequential imperative programming language syntax, semantics, Hoare logics and verification environment. Archive of Formal Proofs
  ST12.Sternagel C, Thiemann R (2012) Certification of nontermination proofs. In: Beringer L, Felty AP (eds) ITP 2012. LNCS, vol 7406. Springer, pp 266–282
  Sto77.Stoy JE (1977) Denotational semantics: the scott-strachey approach to programming language theory. MIT Press
  SW09.Schirmer N, Wenzel M (2009) State spaces—the locale way. ENTCS 254: 161–179
  
• 作者单位：Alasdair Armstrong (1)
  Victor B. F. Gomes (1)
  Georg Struth (1)
  
  1. Department of Computer Science, University of Sheffield, Sheffield, UK
  
• 刊物类别：Computer Science
• 刊物主题：Math Applications in Computer Science
  Theory of Computation
  Computational Mathematics and Numerical Analysis
  
• 出版者：Springer London
• ISSN：1433-299X

文摘

We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work.