仕様記述言語OBJ

電総研（現在の産総研）の言語処理研究室の研修生として３ヶ月在籍した時に、あるOBJの論文を渡された。LISP上の言語だった。LISPがあまり得意でなく、LISPを読んでも珍紛漢紛で、C言語でシンタックスチェッカを書いた。

ソフトウェア技術者協会で「OBJの試用経験」という表題で二木厚吉室長と連名で発表させていただいた。
電総研での席は、戸村哲さんの隣で、UNIXのファイルをNFSで共有させていただいた。
戸村さんは、Emacsの多言語処理を行うMuleの開発をされており、日本語変換ソフトTAMAGO（Taihen　Matasete Gomen）も作られていた。
UNIXもあまり得意でなく、PCのVZエディタでプログラミングして、UNIX上でコンパイルしていた。

ソフトウェア技術者協会(SEA: Software Engineer Association)の発表では、なんでシンタックスチェッカ作ったのかが見え透いていたのか、LISPのシステムをCでシンタックスチェッカなんか作るのが不自然だったのか、コンパイラを作りたいという意図が見え見えだったのか、自分では理解できない質問が飛んだ。
二木室長からは、３ヶ月の研修生で、ここまでのものを書いた研修生は過去にいないと言っていただき、質問はピタッと止んだ。発表者の意図に沿わない質問をしても、発表者には何も響かないという経験をした最初で最後の機会だったかもしれない。

残念だったのは、SEAの月刊誌に、「苦労話がきけなかった」という意見が載ったことだった。
SEAの質問も、雑誌の記事も、発表者が、自分の仕事場で、ひどい開発環境で、システムの無駄な管理をさせられていたこと。電総研は、英語の文献、雑誌が図書室に山のようにあり、戸村哲さんの環境を拝見させていただきなら、自分の慣れ親しんだVZエディタでUNIXのコンパイラでコンパイルできるなんて、人生の幸せの絶頂だった。苦労話なんてあるわけがない。
最初の１月は、Small C Compilerのソースコードを入力し、コンパイルに成功したら、
次の１月は、Pascalで書かれたコンパイラの本のPascalのコードをCに変換しながらコンパイルに成功し、
最後の一月で、YaccとLexを使いながらOBJのシンタックスチェッカを作成した。lex部分は、最終的にはCのコードでベタ書きして、lexは使わなかった。

この経験は、その後のC言語教育で、Cコンパイラを書かなきゃ、C言語のことはわからないという趣旨のもと、３ヶ月あればCコンパイラは書けるようになるという自分の経験をもとに３５年間、一貫した指導方針でした。１０人中２人はCコンパイラが書けるようになるものの８割が途中で挫折するのを見て、C Puzzle Bookと、C言語で書かれたゲームの写経の３択

C言語を習得する３つの方法
https://qiita.com/kaizen_nagoya/items/84cab0888c193bba429b

夕食は、「弥の字」で、Muleの開発者の半谷さんや、言語処理研究室の高橋さんたちが会話している内容を聞きながら、「あ、やっぱり」とか、いろいろ電総研で生きていくのに経験しそうな話を小耳にはなみながら幸せな３ヶ月間でした。
筑波で、１軒屋を、鹿児島県工業試験場の方と２人で借りて、１Fが私、２Fが彼氏が使う感じ。
化学専門の彼は、夜中に音をだしてゲームをしたいのでアパートより１軒屋がいいとのことで２人で借りました。筑波は研修生などの短期借りが多いらしく、結構お値打ちで借りれ、出張費用の範囲内でおさまりました。自動車を愛知県から運んで、借りた場所から電総研までは数キロありました。通勤渋滞もなく、快適な日々でした。
もう３ヶ月間は、府中の中小企業大学校で、勉強し、デザイナ指導者養成コースを受講しました。都道府県のデザイン部、愛知県の窯業試験場の職員などと一緒にデザインをどう指導するか、特にどういう教材を使うかが参考になりました。
自由課題の日は、渋谷、原宿あたりで、鹿児島県工業試験場の彼氏から借りたCANNONの一眼レフで、写真を撮りまくりました。渋谷、原宿あたりでは、カメラを向けると半分ちかくの方はポーズをとってくれました。女子中学生、女子高生などは、きゃっきゃ言って、群がってくれたりもしました。１日で１００枚以上の写真を撮り、ファインダから切り取った東京の風景を、いかに名古屋に伝えることができるかを学びました。
山形の繊維工場の見学では、工場の経営者がさくらんぼ畑の所有者で、昼にはとりたいだけさくらんぼをつんで食べてよいという特典がありました。作成した報告書は、工場の経営者の理解がえられず、一部削除されてしまいました。経営者の方と話をする時間が取れれば、説明できたかもしれません。

OBJシンタックスチェッカ作成の３ヶ月でまなんだこと
1 PascalのコードをCに移植するには、配列の範囲の検査を厳重にする必要がある。
現在では、Syntax Checkerで警告がだせて手を加えることができる。
当時は、よくわからず、デバッグモードで空間に余裕があると動くが、デバッグモードでないとハングするという代物だった。TMCのコーディング標準の２nd Opinionを求められ、MISRA Cのチェッカなどを４−５種類ためしながら学んだ。Cの規格策定団体へのリエゾンでMISRAとともに参加したりした。
2 コンパイラの最適化はちゃんと理論をなぞらないとだめだってなった。
FORTRANの最適化を手でやったときに、FORTRANコンパイラの最適化と矛盾が生じることがわかっていたはずで、ちゃんと最適化の勉強すればよかったと反省。後の祭り。
3 英語の雑誌、書籍は網羅的に読む。
電総研の図書室は天国。読みたい本がならんでいた。本屋さんから、みはからいで来た書籍を軒並み読んだ。のちに、amazonに感想を１万冊あげるにあたって、この時に毎日１冊読む習慣は、中学校の夏休みに１日１冊読む習慣からきているものの、最新技術で無料っていうとこがすごいかもってなった。
4 開発環境と言語
Muleの開発メンバの横で、VZエディタで作業しているのは流石につらかった。
手が慣れており、きりはりの速度が違うって心の中で言い訳しつつ。
NFSでUNIXの開発環境を支えるのは楽勝。

祝：ソースコード公開：VZエディタ移植の方法と成果。註釈 coding(123)
https://qiita.com/kaizen_nagoya/items/5551be98dcbed8f41949

誰でもわかるVZエディタ。0から始める。
https://qiita.com/kaizen_nagoya/items/afe6c4cdccbfdd94baab

5 割り込みがない。
仕事時間中の割り込みがないのは最高。
自分の仕事場でないので、お客様からの電話は０。
学生の指導は、パソコン通信でやりとり。
MS-DOSのFDを、UNIXに移植する作業は、自分が両方を触りながらReviewするのは最高。

OBJ2概観　二木厚吉　電子技術総合研究所言語処理研究室

An Overview on OBJ2, Kokichi Futatsugi
https://researchmap.jp/multidatabases/multidatabase_contents/download/231120/3e1b44bee26c7d7ba02eb6ca5d0c5583/40439?col_no=2&frame_id=576083

0BJ2言語を、そのBNFに基づいて概説する。0BJ2は、 最近のプログラミング方法論から強い影響を受けた、超高水準の 論理型言語であり、抽象データ型、パラメータ化されたモジュー ル、 対話型プログラミングなどを可能にする機能を特徴とする. OBJ 2は、述諸診理でなく等式論理を基礎にした関数型言語で あり、項書き換えシステムに基づく筒明な操作的意味を持つ。

An Overview of OBJ2 (in English)
Kokichi FUTATSUGI
Electrotechnical Laboratory
1-1-4 Umezono, Tsukuba Science City
Ibaraki 305, JAPAN
An overview of the programming language OBJ2 is given based of its BNF definition. OBJ2 is a logic based ultra-high level programming language that has been strongly influenced by modern programming methodology. In particular, it provides facilities for user definable abstract data types, parameterized abstract objects, and interactive programming. OBJ2 is a functional programming language based on equational logic, rather than first order logic; because equations can be interpreted directly as rewrite rules and it is easy to see their computational significance as well as their logical significance.

An Overview of OBJ2
Kokichi FUTATSUGI
Electrotechnical Laboratory
1-1-4 Umezono, Tsukuba Science City
Ibaraki 305, JAPAN

1. introduction

OBJ2 is a logic based ultra-high level programming language that has been strongly influenced by modern programming methodology. In particular, it provides facilities for user definable abstract data types, parameterized abstract objects, and interactive programming. OBJ2 is a functional programming language based on equational logic, rather than first order logic; because equations can be interpreted directly as rewrite rules and it is easy to see their computationa1 significance as well as their logical significance.
This account is prepared to explain OBJ2 language based on its BNF definition and supposed to be a preliminary language manual. Principles of OBJ2 and a more example oriented account of OBJ2 can be found in [1]and [2].
OBJ2 system is designed to be highly interactive and flexible. To achieve these goalsz OBJ2!s syntax is designed so that each major syntactic category corresponds to commands whose function is either to enter information into or to get some information from the OBJ2 database. As a result, the major syntactic categories of OBJ2 language are named command, Cmd for short.
OBJ21s top level entities are objects, theories and views. The main body of the OBJ2 language is composed of commands which enter these entities. Every command can also be seen as a description of each entity. We will mainly explain these three kinds of commands in the following sections.
The following convention will be used in BNF notations throughout this document.

	nonterminal symbols
!	alternative separator
exp,...	one or more exp's separated by commas
{el,...,en}	choice of exactly one of el...en
{{exp}}	zero or one exp; exp is optional
(exp)	parentheses used for grouping syntactic expressions
"( " ")"	parentheses used as terminal symbols
[exp]	equivalent to (exp： "("exp")" )
"[" "]"	brackets used as terminal symbols
---text	informal but clear definition of syntax used in the right hand of definitions

2. OBJECT AND THEORY COMMANDS

Syntactically object and theory commands are almost same, except theory commands can not contain parameter declarations. This implies that theories can not be parameterized.
[BNF:] The top level syntax of object and theory commands are given as follows. [] ends a BNF part.
::= [ ... ]
::= [{obj,ob,object} <0bjName>
{{}} is]
::=
"[,,(< ParameterName > :: ),..."]"
::=
[{.,jbo,bo,endo,endob,endobj}] ::=
::= [
...
]
::= [{th,theory}
is]
::= [{.,ht,endt,endth}]
::= ::=
!
；
： ： < SubsortsCmd>
： !
: ：
! ! []
We will use the term module to refer to both of object and theory. Each module command, i.e. or , can be seen as a list of several kinds of sub-commands. These sub-commands, except and , declare each component of the module and enter the component into database.
[EX:] The followings are three s which represent the same theory TRIV* (sort Elt .) is an instance of and one of the sub-commands. [] ends an example.
((th TRIV is) (sort Elt .) (ht))
(th TRIV is (sort Elt .).)
th TRIV is sort Elt . endth []
and くThName> should be global. That is, no two module having the same name can not coexist in a single OBJ2 database. If the OBJ2 system encounters or whose name is or which already exist in the database, the system complains about this and the commands is rejected.
Object can be parameterized and each parameter is declared in as "くParameterName> :: くThNameゾ. is local to the which contains the . When the z which uses in the , is given to the system, the should already exist in the database. That is which contains the same in its should already be given to the system.
In general, every name which is referred to in some command should be enrolled into database and represents some entity at the point when the command is given to the OBJ2 system.

2.1.MODULE PART C0MMAN AND THE HIERARCHY OF MODULES

Module part commands are classified into the following four categories. We use the term 1 current module* to indicate the module whose command contains each module part command.

(R-Cmd)	the commands which declares the references to c >ther modules
(S-Cmd)	the commands which declares the current module1 's sorts and subsorts-relations
(O-Cmd)	the commands which declares the current module' 1 s operator
(E-Cmd)	the commands which declares the current module' 's equations

Usually module part commands is ordered following the above order inside module commands.
Almost all modules in OBJ2 is hierarchically structured. That is, modules are defined based on some other modules by referring to those modules. There are three kinds of references in OBJ2. That is, protecting, extending, and using.
Once the references to other modules are settled, the current module can use the sorts and operators of that module to define its own operators and equations. Protecting, extending, and using commands declare and settle the corresponding references to other modules.

[BNF:] ::= [{pr,protecting} .] ::= [{ex,extending} .] ::= [{us,us^ng} .] []

Module expression can be used to create a rather complex module which are composed of already defined modules. However, we postpone the explanation of general module expressions, and will treat the most simple case in which the is the already defined or for the moment.
Semantic differences of protecting, extending ', and using is sketched as follows. That is, protecting preserves both of "no junk" and "no confusion" conditions, extending preserves only "no confusion" condition, whereas using does not preserve both of the conditions of the referred modules. Note that "MODI is protecting M0D2" implies "MODI is extending M0D2" by definition, and the protecting hierarchy is sub-hierarchy of extending hierarchy.

To explain the syntax and semantics of 0BJ2 in more detail, however, it is better to represent each module based on "protecting" and "extending" relation. For this purpose, we will use the following notation to represent hierarchical modules.
MOD = < {{p-MODl p-MODZ ・・・} e-MODl e-M0D2 ... }
SORTS OPS EQS > p-MODl, p-MODl,...are the modules which are protected by module MOD.
e-MODl, e-MOD2, ... are the modules which are extended but by module MOD. SORTS, are the sets of sorts, equations which belong p-MODl, p-MOD2, ... , e-MODl, or e-MOD2, ... . p-MODl p-MOD2 ... e-MODl e-M0D2 ... are called sub-modules of MOD.
Let or do not contain any command in (R-Cmd), then the module which is defined by this module command is represented as:
MOD = < {{}} SORTS OPS EQS >
In this case, the module command should contain sort, operator, and equation sub-commands, which define SORTS, OPS, and EQS respectively. That is, the effect of attaching a sub-command which belong to (S-Cmd), (O-Cmd), or (E-Cmd) is to add some element to SORTS, OPS, or EQS. [Notice: and can not necessarily be understood in this way. We will explain the effects of these command latter.]
To explain the effect of (R-Cmd), we will show what kind of the module hierarchy of the form (1)is obtained by attaching a sub-command of this kind, i.e. by attaching , , or . These are defined as follows.
Let
MODI=< {{p-MODll p-M0D12 ...} e-MODll e-M0D12 ... }
SORTS1 OPS1 EQS1 >
and the current module before attaching a sub-command in (R-Cmd) is shown like:
< {{p-MODl p-MOD2 ...}
e-MODl e-M0D2 ... }
SORTS OPS EQS >

[1] if the sub-command of the form:

protecting MODI・
is attached, then the current module after that becomes as:
< {{p-MODl p-M0D2 ...
MODI p-MODl1 p-M0D12 ... }
e-MODl e-M0D2 ...
e-MODll e-M0D12 ... }
SORTS OPS EQS >

[2] if the sub-command of the form:

extending MODI.
is attached, then the current module after that becomes as:
< {{p-MODl p-M0D2 ... }
e-MODl e-M0D2 ...
MODI p-MODll p-M0D12 ...
e-MODll e-M0D12 ... }
SORTS OPS EQS >

[3] if the sub-command of the form:

using MODI.
is attached, then the current module after that becomes as:
< {{p-MODl p-MOD2 ...
p-MODll p-MOD12 ... }
e-MODl e-M0D2 ・・・
e-MODll e-M0D12 ... }
(SORTS U SORTS1) (OPS U OPS1) (EQS U EQS1)>
[Notice:
(A U B) should be read
as (A union B) in set theory] Note that protecting and extending relations are transitive. Note also that "using" has the same effect as expanding the definition of the used module where this command is invoked

12.2. SORTS AND SUBSORTS COMMANDS

[BNF：]
::=
[{sort, sorts,so} ....] []

A sorts command declares the names of the sorts which are introduced into the current module. Let the current module MOD is represented by
< {{p-MODl p- M0D2 ... } e-MODl e-M0D2 ... }
SORTS OPS EQS >
If the sorts command :

sorts SI S2 S3 •

is given, then the current module becomes

< {{p-MODl p-MOD2 ... } e-MOD丄 e-MOD2 ... }
(SORTS U {SI.MOD S2.MOD S3.MOD}) OPS EQS >

The name SI.MOD stands for the sort SI of MOD, and should be unique in a single OBJ2 database. That is, any sort name should be unique when qualified by the module name where the sort is introduced, and the sort is said to "belong" to the module. In this sense, any sort belongs to exactly one module. This is exactly same for both of operators and equations.
Sometimes, sorts, operators, or equations which belong to one of the sub-modules of a module MOD are also said to belong to MOD. Semantically this usage of the term "belong" is natural,for you would like to think of the "belong relation" transitive. This is, however, contradict to the original definition of "belong" and we will use "directly belongH instead of "belong" to mean the original sense of belong. The term "belong" is reserved to mean the "transitive belong". And so, we should say that all sorts, operators, and equations "directly belong" to exactly one module.
A subsorts command declare the subset relations between the sorts which belong the current module.

[BNF:]
::=
[{subsorts,ss} (... <)...
....]
::= ! . くModName> ::= ； ；< ParameterName > []

For example if the subsorts command:

subsorts SI S2 < S3 .

is given, then the sorts SI and S2 are declared to be subset of the sort S3. If the sort SI is declared to be subset of the sort S2Z SI is said to be "subsortn of S2. The subsort relation is transitive and should not be cyclic. That is, any sort should not be a subsort of itself.
As you can imagine, the command:

Sil S12 ...
< S21 S22 ...
< ...
< Snl Sn2 ....

is equivalent to

subsorts S(n-1)1
subsorts S(n-1)1
subsorts S(n-1)2
subsorts S(n-1)2

Any which appears after the key word "subsorts" should identify a unique sort among the sorts which belong to the current module. The most exact way is to use the qualified name like "List.INT-LIST" to point the sort List which directly belong to the module INT-LIST. You can use a sort name to specify a sort if no ambiguity occurs, i.e. if no two sorts with same name belong to the current module.
You can also qualify s by s to distinguish the two sorts with the same name which directly belong to formal parameter theories of a parameterized object.

[EX:]
Obj TABLE[INDEX ：： TRIV, VAL ：： TRIV] is protecting BOOL . sorts Table ErrVal. subsorts Elt.VAL < ErrVal. op empty : -> Table . op put ： Elt.VAL Elt.INDEX Table
-> Table .
op [] : Table Elt.INDEX
-> ErrVal. vars I 11 : Elt.INDEX . var V : Elt.VAL .
var T : Table •
eq : put(V,I,T)[11]二 if I == I1 then V else T[I!] fi .
endo []

2.3. OPERATOR COMMANDS

[BNF：]
::=
{opz operator, operation}
(； ):
{{}} ->
{{}}.
::=
{ops,operators,operations}
(! )...:
{{}} ->
{{}}. []
An operator command declares an operator which is introduced into the current module. Whereas, an operators command declares several operators at a once.
As you may expect, ops (+) (*):
Int Int -> Int .
is equivalent to op (+) : Int Int -> Int . op : Int Int -> Int . op (*) : Int Int -〉 Int .
[BNF:]
::=
"("(： )...")"
::=
Identifiers which contain
no "(",つ”，ソ,，or symbols
::=
::=
Identifiers which contain
no "(ヽ ")”，",n ::= ...
specifies the pattern in which the operator applied. For example, if the addition operator has the pattern (_ + ), then the expression "2 + 3" is supposed to represent the result of applying the addition operator to the two arguments 2 and 3.
You can specify any pattern besides the usual infix, prefix, or postfix patterns for operators. For example, if the operator command:
op ( is greater than ):
Int Int -> Bool.
is already given, the expression "3 is greater then 2" is supposed to represent the boolean value "true" as a result of applying this operator to the arguments 3 and 2. We call it mixfix or distfix pattern.
In writing down s, spaces are required to separate s and s. However, you can omit spaces before and after the delimiter symbols. In OBJ2, the six symbols: "(", ")", "[", "]", "z", and are delimiters. And so, you can write (+), (push_to), (top of_) instead of (__ + ), (push _ to ), (top of ) respectively. Moreover, if the list contains only one element, you can omit the parentheses which enclose it unless the resulting word contains no ":" symbols. That is, you can write, +, push_to, instead of (+), (push to_) respectively? ~You may not, however, write "top of_" or ”一：—" instead of (top of_) or (:).
Any operator should be uniquely identified in a single 0BJ2 database by the following four items. (1) the module name to which the operator directly belongs, (2) the pattern, (3) the arity, and (4) the range, i.e. the sort of its returned value. That is, no two operators having the same four items should not coexist. This implies that you can introduce many overloaded operators and, at the same time, introduce many chances for ambiguities in the parsing of expressions. Especially, we do not recommend to use the module name to distinguish two operators.
By using the power of the operator pattern mechanism, you can defined your own syntax for expressions. As a matter of fact, you can make use of the same power of context free grammars to defined the syntax.
[EX:]
obj SEQ[X ：： TRIV] is protecting BOOL . sorts Seq .
op . : -> Seq .
op : Elt Seq -> Seq .
op head_ : Seq -> Elt . op tail_ : Seq -> Seq . var S S' : Seq .
var E : Elt .
eq : head E S = E . eq : tail E S = S . endo []
The operator pattern is no doubt one of the most powerful feature of 0BJ2. However, it introduces some subtleties into the language. First of all, it requires the full context free parsing with ambiguities. We will explain about this in more detail below where the syntax of s are defined.
You can attach some attributes to operators.
[BNF:]
::=
{"[", at,attr,attribute} ...
{"]",ta,enda,endat,rtta} ::= assoc ! associative ；comm ； commutative ! (id:! identity:) ! memo i ； ::= "("...")" ::=
‹NatNum> ::= 0123.... ::=
[]
Associative, commutative, and identity: attributes are attached to binary operators on some sort, i.e・ the operators having the arity of the form HS1 SI" for some sort SI. "Identity:" declares a constant, i.e. an operator of no arguments, to be the identity of the binary operator.
specifies the strategy in the reduction of OBJ2 terms.
specifies the precedence of operator patterns in the parsing of s.

2.4. EQUATION COMMANDS,

Equation commands introduce new equations into current module.
[BNF：]
::= {var,vars} ... : .
::=
{eq,equation} {{くSort〉}}:
= .
::=
{cq,c-eq,cond-eq} {{}}: = if .
::=
{bq,b-eq,builtin-eq} {{}}: = .
::= ::= ::= ::= Lisp form which
defines the []

A declare s to be variables of sort . s are local in the module command which defines current module and the same should not be used twice even if their s are distinct.
An , , and declares an equation, conditional equation, and builtin equation respectively, which are introduced into the current module.
You may specify the sort of the in all kinds of equation commands by giving . If you specify the , the following is considered to be of sort . If the is omitted, the following is considered to have an operator which directly belongs to the current module as outermost operator. Once the sort of the is determined to be SI, the following considered to be of sort SI or of sort S2 for some subsort S2 of SI, i.e. for the sort S2 < SI.
In you can specify the on which the equation holds. The sort of should be Bool.BOOL which is an 0BJ21s builtin sort.
is considered to be used by builtins by themselves. In , you can write a Lisp form in the which defines the .
, , and should take the form of the OBJ21s . These s should be composed of the operators which belong to the current module. More exactly the terms are defined depending on both of a module and a sort which belongs to the module.
For any module M and the sort S which belongs to M,let Term(M,S) denote the set of terms of the sort S in the context of the module M. Let OPS and SORTS denote the set of operators and sorts which belong to the module M respectively. The operators in OPS are denoted by the four tuples like:
< M >
Notice that the s for standard type operators are transformed to the forms:
(key
in the above definition. For example, if you declare a standard type operator like:

op f : Int Int 一〉 Int .

the of this operator is transformed to

We will define Terms(M,S) for any sort S in SORTS. For doing this we use the notation of [exp] in a similar but slightly different manner as in BNF notations. That is, if we state that [exp] are members of Term(M,S), this means that all of "exp", "(exp)", "((exp))", ... are members of Term(M,S). This notation are used in nested form. For example, if we state that
[key [t]]
are members of Term(M,S), this means that all of the expression “key tn, "key(t)", "key((t))", ... "(key t)", "(key (t))", "(key((t)))", ..., "((key t)", "((key (t)))", "((key ((t))))", ...,... are members of Term(M,S).
Here is the definition of Term(M,S): (1)For any S in SORTS, if an operator of the form:
く M (key) () S>
is in OPS then the expression [key]
are members of Term(M,S).
(2) For any S in SORTS, if x is a variable name of sort S then the expressions
[x] are members of Term(M<S).
(3) If SI is a subsort of S2 then any element of Term(M,SI) is a member of Term(M,S2).
(4) If there is an operator of the form:
< Ml (keyl 一 key2 —・・・ keyi _) (SI S2 7.. Si)~S > 一
in OPS and the expressions:
tl t2 ... ti are members of Term(M,SI)Term(M,S2)...
Term(M,Si ) respectively then the expressions [keyl[tl] key2 [t2]...
keyi [ti]] are members of Term(M,S). The expressions:
tl t2 ... ti are called sub expressions of the obtained expression.
(5) the membership of every expressions in Term(T,S) are guaranteed by only (1),(2),(3) or (4).
In 0BJ2, users can define their own syntax for each operators using the equivalent of the context free grammars, i.e. the operator patterns. There are many chances to introduce ambiguities in parsing the OBJ21s expressions, i.e. an expression may be members of many Term(M,S)s if the M is fixed. The OBJ2 T s basic principle to cope with this is the following definition of well formed expressions of OBJ2.
An expression Exp is well formed in a module M if (1) all of its sub expressions are well formed and (2) there is only one Term(M,S) such that (2.1) Exp is a member of Term(S,M) and (2.2) there are no sort S' such that S' is subsort of S and Exp is also a member of Term(M,S1).
As you can imagine, to parse expression according to the above definition is a little complicated task.

3. VIEW COMMANDS

Instantiating a parameterized object means providing actual objects satisfying each of its requirement theories. In 0BJ2, the actual objects are provided through views, which bind required sorts and operations to those actually provided in such a way that all the axioms of the requirement theory are satisfied. That is, views map the sort and operations in the formal requirement theory to those in the actual object. More generally, a view can map an operator in the formal to a composed operation which is constructed by the operators of the actual.
[BNF:]
::=
{vw,view} of as is ...
{wv,endv,endvw,endview}
::= ： ； く ParameterName >
::=
： : ::=
{so,sort} to .
::=
{op,operator, operation}
{{くSort〉}} : to {{}} : .
::= =::
an expression which is composed only of one operator symbol and variables.
(e.g. X + Y, push Elm to Stack, etc.)
[EX:] Here is an examples of view commands which define a view from total ordered set TOSET to INT, a builtin object of OBJ2 providing integers. Both of TOSET and ェNT have an ordering operator of the form (<)•
view IntDesc of INT as TOSET is sort Elt to Int .
vars X Y : Elt . ,
op Bool:(X < Y) to Bool：(Y < X). endview
The view IntDesc views INT with descending order as a toset; in "(op : X < Y to : Y < X)" the first "く,，is the one from TOSET while the second ”く,' is from INT. []

4. MODULE EXPRESSIONS!

Instantiating a parameterized object . with a view is indicated by replacing the parameter part with the view name. Thus, instantiating the generic sorting object SORTING[X :: TOSET] to sort integers in descending order is indicated by an module expression:
SORTING[IntDesc]
Sometimes a view can be inferred from a partial description, using syntactic similarities between the theory and the object. We call such a view description an abbreviated view； it is a default view if abbreviated to nothing. For example, there is a default view of INT as TOSET that maps Elt to Int and "op (_<_) : Elt Elt -> Bool" to the usual ordering on integers. To instantiate a parameterized object with a default view, it suffices to place the actual in the parameter part. Thus the object defined by the module expression:
SORTェNG[ェNT]
sorts natural numbers in ascending order.
[BNF：]
::=
： [ ,...] ：
：( + )... ::=
I
：
； ::=

• "("...")" ::=
  :: ::=
  "("...")"
  In parsing the , should be tried first. That isA the expression:
  Ml + M2 * (op f to g) should be parsed as
  Ml + (M2 * (op f to g)
  ::= !
  < SortRenameCmd> ::=
  {so,sort} to .
  < OpRenameCmd > ::=
  {op,operator,operation} to ::=

I H(H : {{}} -> n)" ロ M * ( . . . ) is another module expression with sorts and operations renamed according to (...). For example, we may rename the operation sort of SORTING to lex-sort in the module expression SORTING[LEX[ID]] * (op sort to lex-sort.). # 5. OTHER COMMANDS The followings are simple explanations of other OBJ2 commands. invoke the reduction of terms in some specified object [BNF:] ::= {re,red,reduce} in as : ("("くTermゾ)").... [] show the status of the current obj2 database delete some entities form the database dump some entities form the database to files in text form --- read in a file which contains obj2 code save the current obj2 database into a file in Lisp code restore the OBJ2 database which is saved by a create the file which retain all objects, theories, views which are defined in a session read in a file of obj2 code and then append objects, theories, views which are defined in a session invoke Lisp's eval function get into emacs editor # REFERENCES [1]Futatsugi,K., Goguen,J., Jouannaud,J.-P., and Meseguer,J. Principles of 0BJ2. In Proceedings,1985 Symposium of Principles of Programming Languages, ACM, pp.52-66, 1985 [2] Futatsugi,K.,Simple Examples of Parameterlzed Programming in 0BJ2. In Proceedings, 1985 Summer Programming Symposium, IPSJ, pp.55-61, 1985

OCR

Google Drive OCR機能を試してみた（英語）coding(70)
https://qiita.com/kaizen_nagoya/items/5ad1ada6577396601eaa

無料オンラインOCRサービス
https://www.onlineocr.net/ja/
OCR WEB
https://lightpdf.com/jp/ocr
i2ocr
http://www.i2ocr.com/free-online-english-ocr

参考文献一覧作成 ファイルの存在とPDFからの変換
https://qiita.com/kaizen_nagoya/items/8edaf4ca410ef2ccdbc7

<この項は書きかけです。順次追記します。>
This article is not completed. I will add some words and/or centences in order.
Este artículo no está completo. Agregaré algunas palabras en orden.

知人資料

' @kazuo_reve 私が効果を確認した「小川メソッド」
https://qiita.com/kazuo_reve/items/a3ea1d9171deeccc04da

' @kazuo_reve 新人の方によく展開している有益な情報
https://qiita.com/kazuo_reve/items/d1a3f0ee48e24bba38f1

' @kazuo_reve Vモデルについて勘違いしていたと思ったこと
https://qiita.com/kazuo_reve/items/46fddb094563bd9b2e1e

自己記事一覧

Qiitaで逆リンクを表示しなくなったような気がする。時々、スマフォで表示するとあらわっることがあり、完全に削除したのではなさそう。

４月以降、せっせとリンクリストを作り、統計を取って確率を説明しようとしている。
2025年２月末を目標にしている。

一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39

仮説（0）一覧（目標100現在40）
https://qiita.com/kaizen_nagoya/items/f000506fe1837b3590df

Qiita(0)Qiita関連記事一覧（自分）
https://qiita.com/kaizen_nagoya/items/58db5fbf036b28e9dfa6

Error一覧 error(0)
https://qiita.com/kaizen_nagoya/items/48b6cbc8d68eae2c42b8

C++ Support(0)　
https://qiita.com/kaizen_nagoya/items/8720d26f762369a80514

Coding(0) Rules, C, Secure, MISRA and so on
https://qiita.com/kaizen_nagoya/items/400725644a8a0e90fbb0

Ethernet 記事一覧　Ethernet(0)
https://qiita.com/kaizen_nagoya/items/88d35e99f74aefc98794

Wireshark 一覧 wireshark(0)、Ethernet(48)
https://qiita.com/kaizen_nagoya/items/fbed841f61875c4731d0

線網（Wi-Fi）空中線(antenna)(0) 記事一覧(118/300目標)
https://qiita.com/kaizen_nagoya/items/5e5464ac2b24bd4cd001

なぜdockerで機械学習するか 書籍・ソース一覧作成中 (目標100)
https://qiita.com/kaizen_nagoya/items/ddd12477544bf5ba85e2

プログラムちょい替え（0）一覧:4件
https://qiita.com/kaizen_nagoya/items/296d87ef4bfd516bc394

言語処理100本ノックをdockerで。python覚えるのに最適。:10+12
https://qiita.com/kaizen_nagoya/items/7e7eb7c543e0c18438c4

Python(0)記事をまとめたい。
https://qiita.com/kaizen_nagoya/items/088c57d70ab6904ebb53

安全（0）安全工学シンポジウムに向けて: 21
https://qiita.com/kaizen_nagoya/items/c5d78f3def8195cb2409

プログラマによる、プログラマのための、統計(0)と確率のプログラミングとその後
https://qiita.com/kaizen_nagoya/items/6e9897eb641268766909

転職(0)一覧
https://qiita.com/kaizen_nagoya/items/f77520d378d33451d6fe

技術士(0)一覧
https://qiita.com/kaizen_nagoya/items/ce4ccf4eb9c5600b89ea

Reserchmap(0) 一覧
https://qiita.com/kaizen_nagoya/items/506c79e562f406c4257e

物理記事　上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff

量子(0) 計算機, 量子力学
https://qiita.com/kaizen_nagoya/items/1cd954cb0eed92879fd4

数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d

coq(0) 一覧
https://qiita.com/kaizen_nagoya/items/d22f9995cf2173bc3b13

統計(0)一覧
https://qiita.com/kaizen_nagoya/items/80d3b221807e53e88aba

図(0) state, sequence and timing. UML and お絵描き
https://qiita.com/kaizen_nagoya/items/60440a882146aeee9e8f

色(0) 記事100書く切り口
https://qiita.com/kaizen_nagoya/items/22331c0335ed34326b9b

品質一覧
https://qiita.com/kaizen_nagoya/items/2b99b8e9db6d94b2e971

言語・文学記事　１００
https://qiita.com/kaizen_nagoya/items/42d58d5ef7fb53c407d6

医工連携関連記事一覧
https://qiita.com/kaizen_nagoya/items/6ab51c12ba51bc260a82

水の資料集(0)　方針と成果
https://qiita.com/kaizen_nagoya/items/f5dbb30087ea732b52aa

自動車　記事　１００
https://qiita.com/kaizen_nagoya/items/f7f0b9ab36569ad409c5

通信記事１００
https://qiita.com/kaizen_nagoya/items/1d67de5e1cd207b05ef7

日本語（０）一欄
https://qiita.com/kaizen_nagoya/items/7498dcfa3a9ba7fd1e68

英語(0) 一覧
https://qiita.com/kaizen_nagoya/items/680e3f5cbf9430486c7d

音楽　一覧(0)
https://qiita.com/kaizen_nagoya/items/b6e5f42bbfe3bbe40f5d

「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b

鉄道（０）鉄道のシステム考察はてっちゃんがてつだってくれる
https://qiita.com/kaizen_nagoya/items/faa4ea03d91d901a618a

OSEK OS設計の基礎　OSEK(100)
https://qiita.com/kaizen_nagoya/items/7528a22a14242d2d58a3

coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68

官公庁・学校・公的団体（NPOを含む）システムの課題、官（０）
https://qiita.com/kaizen_nagoya/items/04ee6eaf7ec13d3af4c3

「はじめての」シリーズ　 ベクタージャパン　
https://qiita.com/kaizen_nagoya/items/2e41634f6e21a3cf74eb

AUTOSAR(0)Qiita記事一覧, OSEK(75)
https://qiita.com/kaizen_nagoya/items/89c07961b59a8754c869

プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945

LaTeX(0) 一覧　
https://qiita.com/kaizen_nagoya/items/e3f7dafacab58c499792

自動制御、制御工学一覧（０）
https://qiita.com/kaizen_nagoya/items/7767a4e19a6ae1479e6b

Rust(0) 一覧　
https://qiita.com/kaizen_nagoya/items/5e8bb080ba6ca0281927

programの本質は計画だ。programは設計だ。
https://qiita.com/kaizen_nagoya/items/c8545a769c246a458c27

登壇直後版 色使い(JIS安全色) Qiita Engineer Festa 2023〜私しか得しないニッチな技術でLT〜 スライド編 0.15
https://qiita.com/kaizen_nagoya/items/f0d3070d839f4f735b2b

プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945

逆も真：社会人が最初に確かめるとよいこと。OSEK(69)、Ethernet(59)
https://qiita.com/kaizen_nagoya/items/39afe4a728a31b903ddc

統計の嘘。仮説（127）
https://qiita.com/kaizen_nagoya/items/63b48ecf258a3471c51b

自分の言葉だけで論理展開できるのが天才なら、文章の引用だけで論理展開できるのが秀才だ。仮説（136）
https://qiita.com/kaizen_nagoya/items/97cf07b9e24f860624dd

参考文献駆動執筆(references driven writing)・デンソークリエイト編
https://qiita.com/kaizen_nagoya/items/b27b3f58b8bf265a5cd1

「何を」よりも「誰を」。１０年後のために今見習いたい人たち
https://qiita.com/kaizen_nagoya/items/8045978b16eb49d572b2

Qiitaの記事に３段階または５段階で到達するための方法
https://qiita.com/kaizen_nagoya/items/6e9298296852325adc5e

出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840

祝休日・謹賀新年 2025年の目標
https://qiita.com/kaizen_nagoya/items/dfa34827932f99c59bbc

Qiita 1年間をまとめた「振り返りページ」＠2024
https://qiita.com/kaizen_nagoya/items/ed6be239119c99b15828

2024 参加・主催Calendarと投稿記事一覧 Qiita(248)
https://qiita.com/kaizen_nagoya/items/d80b8fbac2496df7827f

主催Calendar2024分析 Qiita(254)
https://qiita.com/kaizen_nagoya/items/15807336d583076f70bc

Calendar 統計
https://qiita.com/kaizen_nagoya/items/e315558dcea8ee3fe43e

LLM 関連 Calendar 2024
https://qiita.com/kaizen_nagoya/items/c36033cf66862d5496fa

Large Language Model Related Calendar
https://qiita.com/kaizen_nagoya/items/3beb0bc3fb71e3ae6d66

博士論文 Calendar 2024 を開催します。
https://qiita.com/kaizen_nagoya/items/51601357efbcaf1057d0

博士論文(0)関連記事一覧
https://qiita.com/kaizen_nagoya/items/8f223a760e607b705e78

coding (101) 一覧を作成し始めた。omake:最近のQiitaで表示しない5つの事象
https://qiita.com/kaizen_nagoya/items/20667f09f19598aedb68

あなたは「勘違いまとめ」から、勘違いだと言っていることが勘違いだといくつ見つけられますか。人間の間違い(human error(125))の種類と対策
https://qiita.com/kaizen_nagoya/items/ae391b77fffb098b8fb4

プログラマの「プログラムが書ける」思い込みは強みだ。３つの理由。仮説（168）統計と確率(17) , OSEK(79)
https://qiita.com/kaizen_nagoya/items/bc5dd86e414de402ec29

出力(output)と呼ばないで。これは状態(state)です。
https://qiita.com/kaizen_nagoya/items/80b8b5913b2748867840

これからの情報伝達手段の在り方について考えてみよう。炎上と便乗。
https://qiita.com/kaizen_nagoya/items/71a09077ac195214f0db

ISO/IEC JTC1 SC7 Software and System Engineering
https://qiita.com/kaizen_nagoya/items/48b43f0f6976a078d907

アクセシビリティの知見を発信しよう！（再び）
https://qiita.com/kaizen_nagoya/items/03457eb9ee74105ee618

統計論及確率論輪講（再び）
https://qiita.com/kaizen_nagoya/items/590874ccfca988e85ea3

読者の心をグッと惹き寄せる7つの魔法
https://qiita.com/kaizen_nagoya/items/b1b5e89bd5c0a211d862

「@kazuo_reve 新人の方によく展開している有益な情報」確認一覧
https://qiita.com/kaizen_nagoya/items/b9380888d1e5a042646b

ソースコードで議論しよう。日本語で議論するの止めましょう（あるプログラミング技術の議論報告）
https://qiita.com/kaizen_nagoya/items/8b9811c80f3338c6c0b0

脳内コンパイラの3つの危険
https://qiita.com/kaizen_nagoya/items/7025cf2d7bd9f276e382

心理学の本を読むよりはコンパイラ書いた方がよくね。仮説（34）
https://qiita.com/kaizen_nagoya/items/fa715732cc148e48880e

NASAを超えるつもりがあれば読んでください。
https://qiita.com/kaizen_nagoya/items/e81669f9cb53109157f6

データサイエンティストの気づき!「勉強して仕事に役立てない人。大嫌い!!」『それ自分かも?』ってなった!!!
https://qiita.com/kaizen_nagoya/items/d85830d58d8dd7f71d07

「ぼくの好きな先生」「人がやらないことをやれ」プログラマになるまで。仮説（37）　
https://qiita.com/kaizen_nagoya/items/53e4bded9fe5f724b3c4

なぜ経済学徒を辞め、計算機屋になったか（経済学部入学前・入学後・卒業後対応） 転職(1)
https://qiita.com/kaizen_nagoya/items/06335a1d24c099733f64

プログラミング言語教育のXYZ。 仮説（52）
https://qiita.com/kaizen_nagoya/items/1950c5810fb5c0b07be4

【24卒向け】9ヶ月後に年収１０００万円を目指す。二つの関門と三つの道。
https://qiita.com/kaizen_nagoya/items/fb5bff147193f726ad25

「【25卒向け】Qiita Career Meetup for STUDENT」予習の勧め
https://qiita.com/kaizen_nagoya/items/00eadb8a6e738cb6336f

大学入試不合格でも筆記試験のない大学に入って卒業できる。卒業しなくても博士になれる。
https://qiita.com/kaizen_nagoya/items/74adec99f396d64b5fd5

全世界の不登校の子供たち「博士論文」を書こう。世界子供博士論文遠隔実践中心 安全(99)
https://qiita.com/kaizen_nagoya/items/912d69032c012bcc84f2

日本のプログラマが世界で戦える16分野。仮説(53),統計と確率(25) 転職(32)、Ethernet(58)
https://qiita.com/kaizen_nagoya/items/a7e634a996cdd02bc53b

小川メソッド　覚え（書きかけ）
https://qiita.com/kaizen_nagoya/items/3593d72eca551742df68

DoCAP（ドゥーキャップ）って何ですか？
https://qiita.com/kaizen_nagoya/items/47e0e6509ab792c43327

views 20,000越え自己記事一覧
https://qiita.com/kaizen_nagoya/items/58e8bd6450957cdecd81

Views１万越え、もうすぐ１万記事一覧 最近いいねをいただいた213記事
https://qiita.com/kaizen_nagoya/items/d2b805717a92459ce853

amazon 殿堂入りNo1レビュアになるまで。仮説(102)
https://qiita.com/kaizen_nagoya/items/83259d18921ce75a91f4

100以上いいねをいただいた記事16選
https://qiita.com/kaizen_nagoya/items/f8d958d9084ffbd15d2a

水道局10年(1976,4-1986,3)を振り返る
https://qiita.com/kaizen_nagoya/items/707fcf6fae230dd349bf

小川清最終講義、最終講義（再）計画, Ethernet(100) 英語(100) 安全(100)
https://qiita.com/kaizen_nagoya/items/e2df642e3951e35e6a53

＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on my individual experience. It has nothing to do with the organization or business to which I currently belong.
Este artículo es una impresión personal basada en mi experiencia personal. No tiene nada que ver con la organización o empresa a la que pertenezco actualmente.

文書履歴(document history)

ver. 0.01 初稿 　20250518

最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。

Thank you very much for reading to the last sentence.

Please press the like icon 💚　and follow me for your happy life.

Muchas gracias por leer hasta la última oración.

Por favor, haz clic en el ícono Me gusta 💚 y sígueme para tener una vida feliz.