Verification of Snapshotable Trees using Access Permissions and Typestate
| Autor: | Hannes Mehnert, Jonathan Aldrich |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
80399 Computer Software not elsewhere classified
FOS: Computer and information sciences Java business.industry Computer science Programming language Modular design computer.software_genre Data structure Abstract interface TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Code (cryptography) business computer Boolean data type Plural computer.programming_language |
| Zdroj: | Mehnert, H & Aldrich, J 2012, ' Verification of Snapshotable Trees using Access Permissions and Typestate ', Lecture Notes in Computer Science, vol. 7304, pp. 187-201 . https://doi.org/10.1007/978-3-642-30561-0_14 Objects, Models, Components, Patterns ISBN: 9783642305603 TOOLS (50) |
| DOI: | 10.1184/r1/6626468 |
| Popis: | We use access permissions and typestate to specify and ver- ify a Java library that implements snapshotable search trees, as well as some client code. We formalize our approach in the Plural tool, a sound modular typestate checking tool. We describe the challenges to verify- ing snapshotable trees in Plural, give an abstract interface specification against which we verify the client code, provide a concrete specification for an implementation and describe proof patterns we found. We also relate this verification approach to other techniques used to verify this data structure. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|