Proving Well-Definedness of JML Specifications with KeY

@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},
  location      = {Karlsruhe, Germany},
  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}
}