Paper Info
Title
Immutable specifications for more concise and precise verification
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.
Year
DOI
Venue
2011
10.1145/2048066.2048096
OOPSLA
Keywords
Field
DocType
immutable specification,current proposal,precise verification,immutability enhanced specification mechanism,immutability guarantee,concise specification,new entailment procedure,better specification,current work,new procedure,immutability annotation,immutability enhanced specification,data structure,separation logic,operational semantics
ENCODE,Data structure,Operational semantics,Separation logic,Logical consequence,Programming language,Computer science,Immutability,Heap (data structure),Soundness
Conference
Volume
Issue
ISSN
46
10
0362-1340
Citations 
PageRank 
References 
4
0.45
10
Authors
2
Name
Order
Citations
PageRank
Cristina David124514.14
Wei-Ngan Chin286863.37