Show simple item record

dc.contributor.author
Kassios, Ioannis T.
dc.contributor.author
Müller, Peter
dc.date.accessioned
2018-03-09T11:13:36Z
dc.date.available
2017-06-13T15:31:27Z
dc.date.available
2018-03-09T11:13:36Z
dc.date.issued
2010
dc.identifier.uri
http://hdl.handle.net/20.500.11850/153103
dc.identifier.doi
10.3929/ethz-a-006843251
dc.description.abstract
Closures, first-class citizen procedures that are able to capture their lexical environment, increase the expressiveness of objectoriented languages such as C#, Scala, and various dynamic languages. However, closures make program specification and verification more difficult. For instance, a verification methodology must allow specifications to describe the behavior of one method relatively to the specification of another method passed as argument, and it must allow specifications to describe the behavior of a closure without exposing its captured state. This paper presents a modular specification and partial correctness verification methodology for closures. Our solution is based on first-order logic and, thus, well suited for automatic verification with SMT solvers. We present an encoding of our methodology in the Boogie program verifier. Using this encoding, we have verified a series of interesting examples that cover the main applications of closures such as delegation patterns and even the creation of custom control flow.
en_US
dc.language.iso
en
en_US
dc.publisher
ETH, Department of Computer Science
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
SPEZIFIKATIONEN (SOFTWARE ENGINEERING)
en_US
dc.subject
VERIFICATION (SOFTWARE ENGINEERING)
en_US
dc.subject
OBJECT-ORIENTED PROGRAMMING (PROGRAMMING METHODS)
en_US
dc.subject
SPECIFICATIONS (SOFTWARE ENGINEERING)
en_US
dc.subject
VERIFIKATION (SOFTWARE ENGINEERING)
en_US
dc.subject
OBJEKTORIENTIERTE PROGRAMMIERUNG (PROGRAMMIERMETHODEN)
en_US
dc.title
Specification and verification of closures
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
dc.date.published
2011
ethz.journal.title
Technical Report / ETH Zurich, Department of Computer Science
ethz.journal.volume
660
en_US
ethz.size
25 p.
en_US
ethz.code.ddc
0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.notes
Technical Reports D-INFK.
en_US
ethz.identifier.nebis
006843251
ethz.publication.place
Zürich
en_US
ethz.publication.status
unpublished
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
ethz.date.deposited
2017-06-13T15:32:24Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp59366b1a3e27434144
ethz.identifier.importid
imp59364d483898e52181
ethz.ecolpid
eth:5050
ethz.ecitpid
pub:42296
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-19T07:13:32Z
ethz.rosetta.lastUpdated
2018-03-09T11:13:39Z
ethz.rosetta.exportRequired
true
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Specification%20and%20verification%20of%20closures&rft.jtitle=Technical%20Report%20/%20ETH%20Zurich,%20Department%20of%20Computer%20Science&rft.date=2010&rft.volume=660&rft.au=Kassios,%20Ioannis%20T.&M%C3%BCller,%20Peter&rft.genre=report&
 Search via SFX

Files in this item

Thumbnail

Publication type

Show simple item record