Please use this identifier to cite or link to this item: https://doi.org/10.1145/2076021.2048096
Title: Immutable specifications for more concise and precise verification
Authors: David, C.
Chin, W.-N. 
Keywords: Languages
Verification
Issue Date: 2011
Source: David, C., Chin, W.-N. (2011). Immutable specifications for more concise and precise verification. ACM SIGPLAN Notices 46 (10) : 359-374. ScholarBank@NUS Repository. https://doi.org/10.1145/2076021.2048096
Abstract: In the current work, we investigate the benefits of immutability guarantees for allowing more flexible handling of aliasing, as well as more precise and concise specifications. Our approach supports finer levels of control that can mark data structures as being immutable through the use of immutability annotations. By using such annotations to encode immutability guarantees, we expect to obtain better specifications that can more accurately describe the intentions, as well as prohibitions, of the method. Ultimately, our goal is improving the precision of the verification process, as well as making the specifications more readable, more precise and as an enforceable program documentation.We have designed and implemented a new entailment procedure to formally and automatically reason about immutability enhanced specifications. We have also formalised the soundness for our new procedure through an operational semantics with mutability assertions on the heap. Lastly, we have carried out a set of experiments to both validate and affirm the utility of our current proposal on immutability enhanced specification mechanism.. Copyright © 2011 ACM.
Source Title: ACM SIGPLAN Notices
URI: http://scholarbank.nus.edu.sg/handle/10635/42214
ISSN: 15232867
DOI: 10.1145/2076021.2048096
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

WEB OF SCIENCETM
Citations

1
checked on Nov 18, 2017

Page view(s)

61
checked on Dec 10, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.