Open access
Date
2011-01Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
Delegation is a very common programming idiom, whereby a task is carried out by a statically unknown part of the program. Delegation enhances the modularity and the extensibility of a program, and, for that reason, is the main ingredient of many important design patterns. Unfortunately, delegation complicates specification and verification: the programmer must either rely on unsuitably weak specifications imposed by behavioral subtyping, or compromise automation by resorting to higherorder logic. In this paper, we present an expressive specification and verification methodology, in which partial correctness reasoning about delegation can be carried out in first order logic, using automated SMT solvers. Show more
Permanent link
https://doi.org/10.3929/ethz-a-006903018Publication status
publishedJournal / series
Technical ReportVolume
Publisher
ETH, Department of Computer ScienceSubject
SPEZIFIKATIONEN (SOFTWARE ENGINEERING); VERIFICATION (SOFTWARE ENGINEERING); SPECIFICATIONS (SOFTWARE ENGINEERING); VERIFIKATION (SOFTWARE ENGINEERING)Organisational unit
03653 - Müller, Peter / Müller, Peter
02150 - Dep. Informatik / Dep. of Computer Science
More
Show all metadata
ETH Bibliography
yes
Altmetrics