Backward Transformation Rules for Programs with Pascal-Like Pointers and Records

Keijiro ARAKI  Takeshi HAYASHI  Kazuo USHIJIMA 

Publication
IEICE TRANSACTIONS (1976-1990)  Vol.E62  No.10  pp.641-648
Publication Date: 1979/10/20
Online ISSN: 
Print ISSN: 0000-0000
Type of Manuscript: PAPER
Category: Programming
Keyword: 


Full Text: PDF(561.7KB)

Summary: 
In this paper we extend Pratt's dynamic logic so as to treat assignment statements concerning Pascal-like pointers and records. We present backward transformation rules for these statements and give the formal justification of the rules by extending Pratt's program-semantics. Properties of programs which manipulate more complex data structures composed of pointers and records (e.g., linked stacks, queues, trees, etc.) can be described in our logic. We prove as an example a partial correctness assertion of a program which treats a linked stack.