¿Qué está mal?

Aviso: Antes de informar sobre un error con la descarga, por favor, prueba el enlace directo: Structural Separation Logic


Debes iniciar sesión para hacer esto.

Structural Separation Logic

Structural Separation Logic

Structural Separation Logic

Puntuación: ---- | 0 votos
| Enviando voto
| ¡Votado!

Detalles del libro:

Editor:Imperial College London
Páginas:307 páginas
Tamaño:4.21 MB
Licencia:Pendiente de revisión


This thesis presents structural separation logic, a novel program reasoning approach for software that manipulates both standard heaps and structured data such as lists and trees. Structural separation logic builds upon existing work in both separation logic and context logic. It considers data abstractly, much as it is exposed by library interfaces, ignoring implementation details.

We provide a programming language that works over structural heaps, which are similar to standard heaps but allow data to be stored in an abstract form. We introduce abstract heaps, which extend structural heaps to enable local reasoning about abstract data. Such data can be split up with structural addresses. Structural addresses allow sub-data (e.g. a sub-tree within a tree) to be abstractly allocated, promoting the sub-data to an abstract heap cell. This cell can be analysed in isolation, then re-joined with the original data. We show how the tight footprints this allows can be refined further with promises, which enable abstract heap cells to retain information about the context from which they were allocated. We prove that our approach is sound with respect to a standard Hoare logic.

We study two large examples. Firstly, we present an axiomatic semantics for the Document Object Model in structural separation logic. We demonstrate how structural separation logic allows abstract reasoning about the DOM tree using tighter footprints than were possible in previous work. Secondly, we give a novel presentation of the POSIX file system library. We identify a subset of the large POSIX standard that focuses on the file system, including commands that manipulate both the file heap and the directory structure. Axioms for this system are given using structural separation logic. As file system resources are typically identified by paths, we use promises to give tight footprints to commands, so that that they do not require all the resource needed to explain paths being used. We demonstrate our reasoning using a software installer example.



Cargando comentarios...

Escaneando listas...

El libro en números

Posición global

posición en categorías

en catálogo desde



Nothing yet...


Nothing yet...

'LIKES' sociales

Nothing yet...



Esto puede tardar un momento


Segmentación por países

Esto puede tardar un momento

Páginas de entrada

Segmentación por sitios web


Esto puede tardar un momento