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

Keijiro Araki; Takeshi Hayashi; Kazuo Ushijima

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

Keijiro Araki, Takeshi Hayashi, Kazuo Ushijima

Advanced Software Engineering

Research output: Contribution to journal › Article › peer-review

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

All Science Journal Classification (ASJC) codes

Engineering(all)

Fingerprint Dive into the research topics of 'BACKWARD TRANSFORMATION RULES FOR PROGRAMS WITH PASCAL-LIKE POINTERS AND RECORDS.'. Together they form a unique fingerprint.

Cite this

@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 = jan,

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 -