Multiple Pre/Post Specifications for Heap-Manipulating Methods

Automated verification plays an important role for high assurance software. This typically uses a pair of pre/post conditions as a formal (but possibly partial) specification of each method before it is systematically verified. In this paper, we advocate for multiple pairs of pre/post conditions to be associated with each method which provides a way for such specification to be used in more scenarios. Multiple pre/post specifications are important for heap-manipulating programs where they can be precisely expressed using separation logic. This work highlights the importance of multiple pre/post specifications, and a methodology to capture them via set of states during proof search.

• Type: Conference
• Year: 2007
• Where: HASE
• Authors: Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin
• Keywords: Control Systems, HASE 2007, Multiple Pre/post Specifications, Pre/post Conditions, Specifications