Specification and Verification of a Transient Stack - Archive ouverte HAL Access content directly
Conference Papers Year :

Specification and Verification of a Transient Stack

(1) , (2) , (1)
1
2

Abstract

A transient data structure is a package of an ephemeral data structure, a persistent data structure, and fast conversions between them. We describe the specification and proof of a transient stack and its iterators. This data structure is a scaled-down version of the general-purpose transient sequence data structure implemented in the OCaml library Sek. Internally, it relies on fixed-capacity arrays, or chunks, which can be shared between several ephemeral and persistent stacks. Dynamic tests are used to determine whether a chunk can be updated in place or must be copied: a chunk can be updated if it is uniquely owned or if the update is monotonic. Using CFML, which implements Separation Logic with Time Credits inside Coq, we verify the functional correctness and the amortized time complexity of this data structure. Our verification effort covers iterators, which involve direct pointers to internal chunks. The specification of iterators describes what the operations on iterators do, how much they cost, and under what circumstances an iterator is invalidated.
Fichier principal
Vignette du fichier
transient-stack.pdf (698.4 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03472028 , version 1 (10-12-2021)

Identifiers

Cite

Alexandre Moine, Arthur Charguéraud, François Pottier. Specification and Verification of a Transient Stack. CPP 2022 - 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. ⟨10.1145/3497775.3503677⟩. ⟨hal-03472028⟩

Relations

268 View
134 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More