論文

査読有り
2008年

Safe modification of pointer programs in refinement calculus

MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS
  • Susumu Nishimura

5133
開始ページ
284
終了ページ
304
記述言語
英語
掲載種別
研究論文(国際会議プロシーディングス)
DOI
10.1007/978-3-540-70594-9_16
出版者・発行元
SPRINGER-VERLAG BERLIN

This paper discusses stepwise refinement of pointer programs in the framework of refinement calculus. We augment the underlying logic with formulas of separation logic and then introduce a pair of new predicate transformers, called separating assertion and separating assumption. The new predicate transformers are derived from separating conjunction and separating implication, which are fundamental logical connectives in separation logic. They represent primitive forms of heap allocation/deallocation operators and the basic pointer statements can be specified by means of them. We derive several refinement laws that are useful for stepwise refinement and demonstrate the use of the laws in the context of correctness preserving transformations that are intended for improved memory usage.
The formal development is carried out in the framework of higher-order logic and is based on Back and Preoteasa's axiomatization of state space and its extension to the heap storage [BP05, Pre06]. All the results have been implemented and verified in the theorem prover PVS.


リンク情報
DOI
https://doi.org/10.1007/978-3-540-70594-9_16
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000257859400016&DestApp=WOS_CPL
ID情報
  • DOI : 10.1007/978-3-540-70594-9_16
  • ISSN : 0302-9743
  • Web of Science ID : WOS:000257859400016

エクスポート
BibTeX RIS