[2] [CITE@ja[情報学広場:情報処理学会電子図書館]], [[<情報処理学会>]], [TIME[2024-10-04T11:45:42.000Z]] <https://ipsj.ixsq.nii.ac.jp/ej/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=132008&item_no=1&page_id=13&block_id=8>


[1] [CITE@ja[情報学広場:情報処理学会電子図書館]], [[<情報処理学会>]], [TIME[2024-10-04T11:31:52.000Z]] <https://ipsj.ixsq.nii.ac.jp/ej/index.php?active_action=repository_view_main_item_detail&page_id=13&block_id=8&item_id=132007&item_no=1>

>等式論理を基盤とする仕様記述言語では, 仕様は項書換え系による操作的意味を持つため簡約手続きによる実行が可能であり, この実行機構を通して仕様の検証が行なわれる。私達は形式的記述(仕様および検証記述)に自然言語等による説明を加えた拡張されたHTML: Forsdonnet (Formal specification document on network)の文章を対象とし, 形式的記述間の制約の記述と, 簡約手続き, 帰納的証明等の実行機能による制約解消を繰り返すことで, ユーザが対話的に仕様の検証を行う環境を構築した。以下でその説明を行う。 

[3] >>1 の [[Emacs/W3]] を使った実装というのはわかるのだけど >>2 の
[[Netscape]] 版はどういうことだろう。 [[CGI]] か何かでやっているのだろうか。
[[JavaScript]] で頑張るにせよ元の [[HTML]] 無変更では使えそうにないけど...

[FIG(data)[ [216] [[HTML要素概説]]

:[F[要素名]]:[CODE[target]]
:[F[要素名]]:[CODE[constraint]]
:[F[要素名]]:[CODE[module]]
:[F[要素名]]:[CODE[modref]]
:日付:[TIME[1997-09-24]]
:説明:
[TIME(jp)[1997-09-24]]の論文によると、
[[Forsdonnet]]
にある。
仕様と検証の形式的記述に使う。
:出典:
[REFS[

-
[DFN[Forsdonnet1]]:
[CITE@ja[等式論理系における制約解消による証明記述の枠組み]],
[DATA(.author)[[[瀬尾明志]]]],
[DATA(.author)[[[中川中]]]],
[TIME(.published jp)[1997-09-24]]
<https://ipsj.ixsq.nii.ac.jp/ej/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=132008&item_no=1&page_id=13&block_id=8>
- 
[DFN[Forsdonnet2]]:
[CITE@ja[等式論理系における制約解消による証明支援環境構築の試み]],
[DATA(.author)[[[井上直]]]],
[DATA(.author)[[[石黒正揮]]]],
[DATA(.author)[[[中川中]]]],
[TIME(.published jp)[1997-09-24]],
<https://ipsj.ixsq.nii.ac.jp/ej/index.php?active_action=repository_view_main_item_detail&page_id=13&block_id=8&item_id=132007&item_no=1>

]REFS]
:注釈:
-
[DFN@en[Forsdonnet]]
Formal specification document on network。
「形式的記述(仕様および検証記述)に自然言語等による説明を加えた拡張されたHTML」
と説明されている。[[等式論理]]に基づく[[仕様記述言語]]を
[[HTML]] に組み込んだもので、 [[Emacs/W3]] 
を拡張した実装があった。
[SRC[Forsdonnet1]]
[SRC[Forsdonnet2]]

]FIG]