Memoirs of the Graduate School of Science and Engineering Shimane University. Series A

Memoirs of the Graduate School of Science and Engineering Shimane University. Series A 33
1999-12-24 発行


A Formal Expression of Program Structures wrth Algebra
Satou, Tadamasa
While studying properties of programs in designing and reviewing processes, operations such as transformation or development would be done. There is an approch of formalizing the operations with an algebra,such as the regular expression(RE). In this case the strategic and technical viewpoints would beimportant to develop it as methods. In the strategic one it could process the part of program semantics,while it could reduce restrictions to apply an algebra in the technical one.
This paper presents two proposals to do so. Firstly,an idea to seperate a program mto two parts; mechanisms and a structure,to apply an algebra to the structure alone. A structue of a program is the non deterministic maximum possible range,while the mechanisms could make constraint to it to be detemimstic one to be desired. Secondly it is an extension of RE by adding a break for iterations,as that RE may be applied to all kinds ofiterations. It points out that the break enables program structures with continuous iteration structures inω-RE to be developed into pre-tested or post-tested ones in Kleene closures,along with that RE can be applied to breaks in pre-tested or post-tested iterations.

プログラム処理の設計や審査において,処理の変形や展開といった操作が行われるが,この操作を代数(正規表現)によって形式化して扱う考えがある.この場合,方法論として実現するには基本的な考えの確立と技術的な裏付けが大切である 基本的な考えとしては,プログラムの意味を反映した部分が代数で扱えるようにすることであるし,技術上は,継続繰返しや打切りが扱えないなどの正規表現の制約を解消することである.
 本論文では,このための工夫として二つの提案を行う. 一つは基本的な考えで,プログラムを構造と機構に分け,構造の方に代数を適用しようとするものである.「構造」はプログラムのもつ動作の最大範囲であり,機構はこの「構造」に制約を与えて目的とするプログラム動作を規定する.もう一つは技術面で,繰返しの打切りを形式化に正規表現の拡張である.打切りの形式化によって,ω−正規表現の無限列で表したプログラム継続繰返し構造がクリーネの閉包の正規表現の前判定と後判定の繰返し構造に展開できることを指摘するとともに,正規表現の繰返し構造における打切りについても正規表現で扱えることを示す.