Название: Structural Separation Logic Автор: Adam Douglas Wright Издательство: Imperial College London Год: 2013 Формат: pdf Страниц: 307 Размер: 4,2 mb. Язык: English
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.
Exact Solutions for Buckling of Structural Members Название: Exact Solutions for Buckling of Structural Members Автор: C.M. Wang, C.Y. Wang, J.N. Reddy Издательство: CRC Press Год: 2005 Формат: PDF...
Structural Analysis of Complex Networks Название: Structural Analysis of Complex Networks Автор: Matthias Dehmer Издательство: Birkh?user Год: 2010 Формат: PDF Размер: 5 Мб Язык:...
Data Structures Succinctly Part 2 Название: Data Structures Succinctly Part 2 Автор: Robert Horvick Издательство: Syncfusion Inc. Год: 2013 Формат: pdf Страниц: 126 Размер: 2.4 mb...
Навигация
Вход на сайт
Реклама
Structural Separation Logic 
