Proving Well-Definedness of JML Specifications with KeY

Study Thesis

Author(s):Michael Kirsten
School:ITI Schmitt, Karlsruhe Institute of Technology
Year:2013
PDF:

Abstract

Specification methods in formal program verification enable the enhancement of source code with formal annotations as to formally specify the behaviour of a program. This is a popular way in order to subsequently prove software to be reliable and meet certain requirements, which is crucial for many applications and gains even more importance in modern society. The annotations can be taken as a contract, which then can be verified guaranteeing the specified program element – as a receiver – to fulfil this contract with its caller. However, these functional contracts can be problematic for partial functions, e.g., a division, as certain cases may be undefined, as in this example a division by zero. Modern programming languages such as Java handle undefined behaviour by casting an exception.
There are several approaches to handle a potential undefinedness of specifications. In this thesis, we chose one which automatically generates formal proof obligations ensuring that undefined specification expressions will not be evaluated.
Within this work, we elaborate on so-called Well-Definedness Checks dealing with undefinedness occurring in specifications of the modelling language JML/JML* in the KeY System, which is a formal software development tool providing mechanisms to deductively prove the before mentioned contracts. Advantages and delimitations are discussed and, furthermore, precise definitions as well as a fully functional implementation within KeY are given. Our work covers the major part of the specification elements currently supported by KeY, on the higher level including class invariants, model fields, method contracts, loop statements and block contracts. The process of checking the well-definedness of a specification forms a preliminary step before the actual proof and rejects undefined specifications. We further contribute by giving a choice between two different semantics, both bearing different advantages and disadvantages. The thesis also includes an extensive case study analysing many examples and measuring the performance of the implemented Well-Definedness Checks.

BibTeX

@MastersThesis{KirstenStA2013,
  author	= {Michael Kirsten},
  title		= {Proving Well-Definedness of {JML} Specifications with {\KeY}},
  school	= {ITI Schmitt, Karlsruhe Institute of Technology},
  month		= nov,
  year		= {2013},
  abstract      = {Specification methods in formal program verification enable the enhancement of 
  		   source code with formal annotations as to formally specify the behaviour of a 
  		   program. This is a popular way in order to subsequently prove software to be 
  		   reliable and meet certain requirements, which is crucial for many applications 
  		   and gains even more importance in modern society. The annotations can be taken 
  		   as a contract, which then can be verified guaranteeing the specified program 
  		   element – as a receiver – to fulfil this contract with its caller. However, 
  		   these functional contracts can be problematic for partial functions, e.g., 
  		   a division, as certain cases may be \emph{undefined}, as in this example a 
  		   division by zero. Modern programming languages such as Java handle 
  		   \emph{undefined} behaviour by casting an exception.
  		   \newline

  		   There are several approaches to handle a potential \emph{undefinedness} of 
  		   specifications. In this thesis, we chose one which automatically generates 
  		   formal proof obligations ensuring that \emph{undefined} specification 
  		   expressions will not be evaluated.
  		   \newline

  		   Within this work, we elaborate on so-called \emph{Well-Definedness Checks} 
  		   dealing with \emph{undefinedness} occurring in specifications of the modelling 
  		   language JML/JML^\ast in the {\KeY} System, which is a formal software development 
  		   tool providing mechanisms to deductively prove the before mentioned contracts. 
  		   Advantages and delimitations are discussed and, furthermore, precise definitions 
  		   as well as a fully functional implementation within {\KeY} are given. Our work 
  		   covers the major part of the specification elements currently supported by {\KeY}, 
  		   on the higher level including class invariants, model fields, method contracts, 
  		   loop statements and block contracts. The process of checking the 
  		   \emph{well-definedness} of a specification forms a preliminary step before the 
  		   actual proof and rejects \emph{undefined} specifications. We further contribute 
  		   by giving a choice between two different semantics, both bearing different 
  		   advantages and disadvantages. The thesis also includes an extensive case study 
  		   analysing many examples and measuring the performance of the implemented 
  		   \emph{Well-Definedness Checks}.},
  language	= {english},
  type		= {Studienarbeit}
}