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},
  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}
}