loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First International Conference on Software Engineering and Formal Methods (SEFM'03)
Program Verification Using Change Information
Brisbane, Australia
September 22-September 27
ISBN: 0-7695-1949-0
Bernhard Beckert, Universität Karlsruhe
Peter H. Schmitt, Universität Karlsruhe
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, also information is 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.
Citation:
Bernhard Beckert, Peter H. Schmitt, "Program Verification Using Change Information," sefm, pp.91, First International Conference on Software Engineering and Formal Methods (SEFM'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.