抄録
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 |
| 外部発表 | Yes |
Fingerprint
All Science Journal Classification (ASJC) codes
- Engineering(all)
これを引用
BACKWARD TRANSFORMATION RULES FOR PROGRAMS WITH PASCAL-LIKE POINTERS AND RECORDS. / Araki, Keijiro; Hayashi, Takeshi; Ushijima, Kazuo.
：: Transactions of the Institute of Electronics and Communication Engineers of Japan, Section E (English), 巻 E62, 番号 10, 01.01.1979, p. 641-648.研究成果: ジャーナルへの寄稿 › 記事
}
TY - JOUR
T1 - BACKWARD TRANSFORMATION RULES FOR PROGRAMS WITH PASCAL-LIKE POINTERS AND RECORDS.
AU - Araki, Keijiro
AU - Hayashi, Takeshi
AU - Ushijima, Kazuo
PY - 1979/1/1
Y1 - 1979/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0018533235&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0018533235&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:0018533235
VL - E62
SP - 641
EP - 648
JO - Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E
JF - Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E
SN - 0387-236X
IS - 10
ER -