Formally Specifying Dynamic Data Structures for Embedded Software Design: an Initial Approach

In the embedded, multimedia community, designers deal with data management at different levels of abstraction ranging from abstract data types and dynamic memory management to physical data organisations. In order to achieve large reductions in energy consumption, memory footprint, and/or execution time, data structure related optimizations are a must. However, the complexity of describing and implementing such optimized implementations is immense. Hence, a strong, practical need is present to unambiguously (i.e. mathematically) describe these complicated dynamic data organisations.The objective of this article is to formally describe data structures and access operations -or dynamic data structures for short- that we have implemented in prior, application-related work. We do this by (a) extending the syntax and semantics of Separation Logic -a logic developed recently in the program verification community- and (b) using it as a specification language for our applications. The short-term benefit of this work is that it allows the embedded software designer to unambiguously express and hence more easily explore low cost, dynamic data structures. In practice this means that the designer can clearly reason and consequently implement nontrivial but optimal dynamic data structures. The benefit in the long term is that it provides an avenue for future optimizing compilers to increase the global scope of optimizations that are related to dynamic data management