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