A Verified Implementation of the Bounded List Container
| Autor: | Raphaël Cauderlier, Mihaela Sighireanu |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Correctness
Computer science Programming language 020207 software engineering 02 engineering and technology Separation logic computer.software_genre Data structure Tree traversal Doubly linked list Bounded function 0202 electrical engineering electronic engineering information engineering Algebraic data type 020201 artificial intelligence & image processing computer Heap (data structure) |
| Zdroj: | Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783319899596 TACAS (1) |
| Popis: | This paper contributes to the trend of providing fully verified container libraries. We consider an implementation of the bounded doubly linked list container which manages the list in a fixed size, heap allocated array. The container provides constant time methods to update the list by adding, deleting, and changing elements, as well as cursors for list traversal and access to elements. The library is implemented in C, but we wrote the code and its specification by imitating the ones provided by GNAT for the standard library of Ada 2012. The proof of functional correctness is done using VeriFast, which provides an auto-active verification environment for Separation Logic extended with algebraic data types. The specifications proved entail the contracts of the Ada library and include new features. The verification method we used employs a precise algebraic model of the data structure and we show that it facilitates the verification and captures entirely the library contracts. This case study may be of interest for other verification platforms, thus we highlight the intricate points of its proof. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|