Java Program Verification via a Hoare Logic with Abrupt Termination

Marieke Huisman, Bart Jacobs

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

78 Citations (Scopus)

Abstract

This paper formalises a semantics for statements and expressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an exception, break, return or continue). This extends the traditional semantics underlying e.g. Hoare logic, which only distinguishes termination and non-termination. An extension of Hoare logic is elaborated that includes means for reasoning about abrupt termination (and side-effects). It prominently involves rules for reasoning about while loops, which may contain exceptions, breaks, continues and returns. This extension applies in particular to Java. As an example, a standard pattern search algorithm in Java (involving a while loop with returns) is proven correct using the proof-tool PVS.
Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering, Third Internationsl Conference, FASE 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings
EditorsT. S. E. Maibaum
PublisherSpringer Singapore
Pages284-303
Number of pages20
DOIs
Publication statusPublished - 2000
Externally publishedYes
Event3rd International Conference on Fundamental Approaches to Software Engineering, FASE 2000 - Berlin, Germany
Duration: 25 Mar 20002 Apr 2000
Conference number: 3

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1783

Conference

Conference3rd International Conference on Fundamental Approaches to Software Engineering, FASE 2000
Abbreviated titleFASE 2000
CountryGermany
CityBerlin
Period25/03/002/04/00

Fingerprint

Dive into the research topics of 'Java Program Verification via a Hoare Logic with Abrupt Termination'. Together they form a unique fingerprint.

Cite this