Abstract
This paper extends V. Pratt's dynamic logic so as to treat assignment statements concerning Pascal-like pointers and records. It presents backward transformation rules for these statements and gives 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 the logic. The authors prove as an example a partial correctness assertion of a program which treats a linked stack.
| Original language | English |
|---|---|
| Pages (from-to) | 641-648 |
| Number of pages | 8 |
| Journal | Transactions of the Institute of Electronics and Communication Engineers of Japan, Section E (English) |
| Volume | E62 |
| Issue number | 10 |
| Publication status | Published - Jan 1 1979 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Engineering(all)
Cite this
Araki, K., Hayashi, T., & Ushijima, K. (1979). BACKWARD TRANSFORMATION RULES FOR PROGRAMS WITH PASCAL-LIKE POINTERS AND RECORDS. Transactions of the Institute of Electronics and Communication Engineers of Japan, Section E (English), E62(10), 641-648.