Paper Info
Title
Tracking behavioral constraints during object-oriented software evolution
Abstract
An intrinsic property of real world software is that it needs to evolve. The software is continuously changed during the initial development phase, and existing software may need modifications to meet new requirements. To facilitate the development and maintenance of programs, it is an advantage to have programming environments which allow the developer to alternate between programming and verification tasks in a flexible manner and which ensures correctness of the final program with respect to specified behavioral properties. This paper proposes a formal framework for the flexible development of object-oriented programs, which supports an interleaving of programming and verification steps. The motivation for this framework is to avoid imposing restrictions on the programming steps to facilitate the verification steps, but rather to track unresolved proof obligations and specified properties of a program which evolves. A proof environment connects unresolved proof obligations and specified properties by means of a soundness invariant which is maintained by both programming and verification steps. Once the set of unresolved obligations is empty, the invariant ensures the soundness of the overall program verification.
Year
DOI
Venue
2012
10.1007/978-3-642-34026-0_19
ISoLA (1)
Keywords
Field
DocType
final program,verification task,verification step,flexible development,specified property,overall program verification,object-oriented software evolution,programming environment,existing software,unresolved proof obligation,programming step,behavioral constraint
Software engineering,Object-oriented programming,Computer science,Correctness,Real-time computing,Class hierarchy,Software,Software product line,Soundness,Software evolution,Software verification
Conference
Citations 
PageRank 
References 
4
0.45
19
Authors
3
Name
Order
Citations
PageRank
Johan Dovland11598.18
Einar Broch Johnsen2107169.56
Ingrid Chieh Yu316418.53