Please login using the form on menu list.|
It is required to login for Full-Text PDF.
Backward Transformation Rules for Programs with Pascal-Like Pointers and Records
IEICE TRANSACTIONS (1976-1990) Vol.E62 No.10 pp.641-648
Publication Date: 1979/10/20
Print ISSN: 0000-0000
Type of Manuscript: PAPER
Full Text: PDF(561.7KB)
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.