Temporary Read-Only Permissions for Separation Logic

Arthur Charguéraud 1, 2 François Pottier 3
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : We present an extension of Separation Logic with a general mechanism for temporarily converting any assertion (or "permission") to a read-only form. No accounting is required: our read-only permissions can be freely duplicated and discarded. We argue that, in circumstances where mutable data structures are temporarily accessed only for reading, our read-only permissions enable more concise specifications and proofs. The metatheory of our proposal is verified in Coq.
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

https://hal.inria.fr/hal-01408657
Contributeur : Arthur Charguéraud <>
Soumis le : lundi 5 décembre 2016 - 11:16:31
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : mardi 21 mars 2017 - 09:37:02

Fichier

readonlysep.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01408657, version 1

Citation

Arthur Charguéraud, François Pottier. Temporary Read-Only Permissions for Separation Logic. 2016. 〈hal-01408657v1〉

Partager

Métriques

Consultations de la notice

54

Téléchargements de fichiers

21