Program verification using change information

Author

Beckert, Bernhard ; Schmitt, Peter H.

Author_Institution

Inst. for Logic, Complexity, & Deduction Syst., Karlsruhe, Germany

fYear

2003

fDate

22-27 Sept. 2003

Firstpage

91

Lastpage

99

Abstract

We propose an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, information is also provided on which parts of the state are not changed by running the program. This is done in the form of modifier sets. We present a precise semantics of modifier sets and theorems on how to use them in program-correctness proofs. This technique has been implemented as part of the KeY system.

Keywords

Java; formal specification; program verification; programming language semantics; software tools; Java card; KeY system; change information; design-by-contract approach; formal specification; formal verification; modifier sets; program verification; software development; unified modeling language; Algorithm design and analysis; Contracts; Formal specifications; Gold; In vitro; Java; Logic design; Programming; Specification languages; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering and Formal Methods, 2003.Proceedings. First International Conference on

Conference_Location

Brisbane, Queensland, Australia

Print_ISBN

0-7695-1949-0

Type

conf

DOI

10.1109/SEFM.2003.1236211

Filename

1236211