From Specification to Proof Obligations

Buchkapitel

Autor(en):Daniel Grahl und Mattias Ulbrich
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:10001
Teil:II: Specification and Verification
Kapitel:8
Jahr:2016
Seiten:243-287
URL:http://dx.doi.org/10.1007/978-3-319-49812-6_8
DOI:10.1007/978-3-319-49812-6_8
Links:

Abstract

The calculus of the KeY prover operates on the logic JavaDL while Java programs are specified using the Java Modeling Language (JML). This chapter builds a formal bridge between the two logical languages by providing a denotational formal semantics for JML, translating expressions and contracts to formulas in JavaDL. Proof obligations which entail the correctness of contracts are defined for functional and dependency contracts. The issue of well-definedness of JML contracts is discussed and a formulation of a proof condition is presented.

BibTeX

@incollection{GrahlUlbrich2016,
  author    = {Daniel Grahl and Mattias Ulbrich},
  title     = {From Specification to Proof Obligations},
  booktitle = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice},
  pages     = {243--287},
  chapter   = {8},
  part      = {II: Specification and Verification},
  year      = {2016},
  month     = dec,
  url       = {http://dx.doi.org/10.1007/978-3-319-49812-6_8},
  doi       = {10.1007/978-3-319-49812-6_8},
  series    = {Lecture Notes in Computer Science},
  volume    = {10001},
  publisher = {Springer}
}