BACKWARD TRANSFORMATION RULES FOR PROGRAMS WITH PASCAL-LIKE POINTERS AND RECORDS.

Keijiro Araki, Takeshi Hayashi, Kazuo Ushijima

研究成果: Contribution to journalArticle査読

抄録

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.

本文言語英語
ページ(範囲)641-648
ページ数8
ジャーナルTransactions of the Institute of Electronics and Communication Engineers of Japan, Section E (English)
E62
10
出版ステータス出版済み - 1 1 1979

All Science Journal Classification (ASJC) codes

  • 工学(全般)

フィンガープリント

「BACKWARD TRANSFORMATION RULES FOR PROGRAMS WITH PASCAL-LIKE POINTERS AND RECORDS.」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル