[2] 情報学広場:情報処理学会電子図書館, <情報処理学会>, 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] 情報学広場:情報処理学会電子図書館, <情報処理学会>, 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 無変更では使えそうにないけど...