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

Keijiro Araki, Takeshi Hayashi, Kazuo Ushijima

研究成果: ジャーナルへの寄稿記事

抄録

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

Data structures
Semantics

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.

研究成果: ジャーナルへの寄稿記事

@article{7a012172c1ee47fe918163157f84c03a,
title = "BACKWARD TRANSFORMATION RULES FOR PROGRAMS WITH PASCAL-LIKE POINTERS AND RECORDS.",
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.",
author = "Keijiro Araki and Takeshi Hayashi and Kazuo Ushijima",
year = "1979",
month = "1",
day = "1",
language = "English",
volume = "E62",
pages = "641--648",
journal = "Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E",
issn = "0387-236X",
number = "10",

}

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 -