- 集合論に基づいた言語を作りたい
402 ：１[sage]：2014/10/01(水) 06:02:07.09 ID:0+f79Okt - >>401
VDM 書いたものが実装にならない
集合論プログラミング 書いたものが実装になる
と思い込んでたからな。
どっちも書いたものが実装にならないならあんまり俺の趣味じゃないなぁ。
集合論プログラムは書いたものが実装になってもよさそうなほど
論理を詰めていたように見えたが気のせいだったか。
|
- 集合論に基づいた言語を作りたい
406 ：1[sage]：2014/10/01(水) 19:43:26.77 ID:0+f79Okt - >>403
どうゆう意味で実行可能なの？
他のプログラムの外付けアサート的な動作しかできないのかと思いこんでいたが。
VDM単体で動くの？
>>404
俺をおだてても木には登れんぞ。
集合論プログラムのコンパイラを作るなんて俺の実力じゃとても出来そうもない。
ユーザーとしてなら使ってみたいが。
>>405
仕様を詳細にするのはやり方がまずいと柔軟性のないプログラムになると思う。
抽象度の高いプログラムで仕様を満たせるならそっちの方がいいと思う。
|
- 集合論に基づいた言語を作りたい
408 ：１[sage]：2014/10/01(水) 20:28:28.86 ID:0+f79Okt - >>407
まじで。英語だからちゃんと読んでないけど>>360のwikiにsqrtの例で
SQRT(x:nat)r:real
post r*r = x
とかいうのがあったからこりゃ単体じゃ実行できないなと思ったんだけど。
早計だったか。
|
- 集合論に基づいた言語を作りたい
410 ：１[sage]：2014/10/01(水) 21:57:06.59 ID:0+f79Okt - >>409
なんか、サンプルプログラムよんでもイメージが湧きづらい。。。
文字列操作の前後のスペースをトリミングとか何やってるのかよく分からん。
[ p | p in set inds org & org(p) <> ' ']がorgの空白でない文字のインデックスの集合で
パターンマッチでその集合の先頭と末尾を取り出してる。
sがorgの空白じゃない最初の文字のインデックスでeがorgの空白じゃない最後の文字のインデックス
でorg(s,...,e)で頭とおしりの空白を取り除いた文字列を返してるってこと？
|
- 集合論に基づいた言語を作りたい
411 ：１[sage]：2014/10/01(水) 22:21:29.56 ID:0+f79Okt - []は集合じゃなくて列か。
|