2ちゃんねる ★スマホ版★ ■掲示板に戻る■ 全部 1- 最新50  

■ このスレッドは過去ログ倉庫に格納されています

完璧なプログラム

1 :デフォルトの名無しさん:02/12/29 10:43
バグが一切無いプログラムを作成することは可能か?
また、「バグが一切無い」と証明する方法は存在するのか?
などを話し合うスレです。

2 :デフォルトの名無しさん:02/12/29 10:44
やっぱりやめた。自由に使ってください。

3 :デフォルトの名無しさん:02/12/29 10:46
↑は偽者です。
年末暇なのはわかりますが、どうか出ていってください。

4 :デフォルトの名無しさん:02/12/29 10:48
何をもってして「バグ」とするの?


5 :1 ◆o/H5.DRW4g :02/12/29 10:49
トリップ付けました。

6 :1 ◆o/H5.DRW4g :02/12/29 10:50
>>4
意図しない動作、不正な参照で死ぬ等。

7 :デフォルトの名無しさん:02/12/29 10:53
>>1
バグが一切無いってのは、どうやったらわかるの?

8 :デフォルトの名無しさん:02/12/29 10:54
>>1
          ┌┬┬┬┐
    ―――┴┴┴┴┴―――――、
.  . /  ̄ ̄ ̄//. ̄ ̄| || ̄ ̄ ̄||| ̄ ||    __________
  ./    ∧// ∧ ∧| ||      |||   ||  /
 [/____(゚_//[ ].゚Д゚,,) ||___|||   || <  こんなのが有りますた
. ||_. *  _|_| ̄ ̄ ∪|.|.       |ヽ.__||  \__________
. lO|o―o|O゜.|二二 |.|    救済病院 ||
 .| ∈口∋ ̄_l__l⌒l_|___|_l⌒l._||
   ̄ ̄`ー' ̄   `ー'  `ー'   `ー'
http://freeserver.kakiko.com/hiroyuki/

9 :1 ◆o/H5.DRW4g :02/12/29 10:55
>>7
いや、だからその方法がないか話し合うスレです。

10 :1 ◆o/H5.DRW4g :02/12/29 10:57
>>8
意味がわからないんですが。

11 :デフォルトの名無しさん:02/12/29 10:57
昔々、チューリングが、「そんな方法ねー」と証明しますた。

12 :デフォルトの名無しさん:02/12/29 10:59
確か、論理的にある程度の規模のプログラムで、
バグの無いプログラムは存在しないってことが証明されてたと思うんだけど、
ソース検索しても出てこない。
う〜む。どうするべかな。

13 :1 ◆o/H5.DRW4g :02/12/29 11:00
>>11
それは知ってますが、だからと言って全く考えないのでは
知能の敗北でしょう。
別に「100%正しい」と証明する必要はありません。

14 :デフォルトの名無しさん:02/12/29 11:03
どれほどテストしてもバグのない証明にはならない。

15 :デフォルトの名無しさん:02/12/29 11:04
>「バグが一切無い」と証明する方法は存在するのか?
>別に「100%正しい」と証明する必要はありません。
どっちだYO!

16 :デフォルトの名無しさん:02/12/29 11:05
なにを持ってバグだといっているんだ、アフォの1は。
要求仕様を満たしていなくてもバグと考えられるし、
性能が出ないのもバグと考えられる。
バグの定義を全て洗い出してから出直してこい、アフォの1よ。

17 :デフォルトの名無しさん:02/12/29 11:07
Lyeeを使えば、すべて仕様ミスになるのでバグはないらしいです。

18 :デフォルトの名無しさん:02/12/29 11:08
バグの定義がバグってる…

19 :デフォルトの名無しさん:02/12/29 11:11
(´-`).。oO(宿題はもう終わったかい?)

20 :デフォルトの名無しさん:02/12/29 11:11
× バグがない
○ バグがばれない

21 :デフォルトの名無しさん:02/12/29 11:12
最近の学校では面白い課題を出すんだね>>1

22 :デフォルトの名無しさん:02/12/29 11:14
>>1-2 またネタスレか

23 :1 ◆o/H5.DRW4g :02/12/29 11:14
>>16
>>6

その他はアホなりにお答えします。

>要求仕様を満たしていない
これはただの未完成です。
バグとは言いません。

>性能が出ない
これはバグとは無関係です。
バグのせいで遅くなることは考えられますが、
アルゴリズムや使用言語、動作環境の変更などで改善されます。

24 :デフォルトの名無しさん:02/12/29 11:16
>>1 Hello, World程度しか表示しないなら可能だろうね。
何をもってバグと定義するかにもよるが。

だがプログラムが巨大化するとそれは不可能としか言いようがない。

XP(eXtreme Progremming)ではバグのないプログラムなどこの世に存在しないと追われている。
XPではプログラムにバグはつき物であることを前提に手法を展開している。
XPとは若干異なるがRUP(Rational Unified Process)もほぼ同様。
従来のWalerFallModelではバグが一切ないことを確認してから前に進むという頑固に見える手法。

バグが100%なくなることはないが少しでもなくそうとするためにオブジェクト指向は生まれたようなもの。

このよから誤差なくならないのと同様に、人間が作る以上、バグは消えない。
新しい機能を追加すれば追加するほどバグは増える。Windowsが恒例だね。
Winはあわてて機能を追加したため今日のセキュリティホールを沢山生み出した。
人(顧客)によって定義するバグは異なるだろう。
あるプログラムにある顧客が欲しがっている機能が存在しない、というだけでそれはその顧客にとってバグである。


25 :デフォルトの名無しさん:02/12/29 11:19
>>1
ソフトウェア工学の勉強しろ!

26 :デフォルトの名無しさん:02/12/29 11:19
>>1
だからおまえはアフォなんだよ。
要求仕様を満たしていないのに出荷されることなんていくらでもある。
それを顧客からみたらバグにしかみえないんだ。
性能もしかり。
暴走したりデータが壊れたときだけがバグと考えているおまえはやはりアフォですね。


27 :1 ◆o/H5.DRW4g :02/12/29 11:22
>>26
わたしがアフォなのは>>16で既にわかりましたが、
もうちょっと建設的な意見をお願いします。
後ろ向きな人なんですか?

28 :デフォルトの名無しさん:02/12/29 11:23
>>1
だからバグの定義をあげろといっとるだろーが。
自分で立てたスレの責任もとれないのか、学生失格だぞ!!

29 :1 ◆o/H5.DRW4g :02/12/29 11:24
>>24
XPとオブジェクト指向だけじゃ不完全ですね。

>>28
>>6

30 :デフォルトの名無しさん:02/12/29 11:26
>27
だから。>>17

31 :デフォルトの名無しさん:02/12/29 11:26
>>1
バグというものを話すのにバグの定義が言えないのでは話しは進まんだろ?
その定義を上げられないなら、まず勉強してきてから出直してください。
マジです。

32 :デフォルトの名無しさん:02/12/29 11:29
>>1
本気ならどこまで扱うかきちんと定義しとかないと考えようがないぞ。
境界領域があいまいなまま話を進めてもまともな議論はできない。


33 :デフォルトの名無しさん:02/12/29 11:32
>>1
だからソフトウェア工学勉強しろって・・・

34 :デフォルトの名無しさん:02/12/29 11:32
>>1
だからクソスレ立てるなって・・・

35 :1 ◆o/H5.DRW4g :02/12/29 11:33
>>30
宣伝ですか?
ケースツールの様ですが、
どういったものかわからないので説明してもらえますか?

>>31
バグの定義は>>6です。

>>32
とりあえず「ロジックのみ」とします。
これまでに上げられた、

・顧客から見た機能不足(未完成納品)
・性能が出ない

は省いてください。

36 :デフォルトの名無しさん:02/12/29 11:33
>>29
> >>24
> XPとオブジェクト指向だけじゃ不完全ですね。
何が?
というかあなた、巨大なプログラム作ったことありますか?
作ってみればバグのないプログラムなど作れないことがわかると思うけど?

37 :デフォルトの名無しさん:02/12/29 11:34
>私は、ソフトウェア設計を組み立てるには二つの方法があるという結論に達した。
>一つは、欠陥がないことが明らかなほど単純にする方法 である。
>もう一つは、明らかな欠陥がないほど複雑にする方法である。

38 :高校生:02/12/29 11:34
いわゆる「正当性の証明」ってやつですよね。

たとえば「a1=a2+a3」という式があったとして
a2=5,a3=6としたら、a1は11になるわけだけど
それが果たして全ての値において成立するかどうか。
それが「正当性の証明」で、本によると数十行程度
なら証明が可能らしいですよ。
 

39 :デフォルトの名無しさん:02/12/29 11:35
>>29 理論だけ並べて現場での実戦経験ない者の発言にしか見えないな。
学生か? 学生だったらプログラマのアルバイト始めて現場を経験してくれ


40 :デフォルトの名無しさん:02/12/29 11:36
バグの定義
意図しない動作、不正な参照で死ぬ等。

無茶言うな

41 :1 ◆o/H5.DRW4g :02/12/29 11:37
>>39
仕事の愚痴はマ板でしてください。

42 :デフォルトの名無しさん:02/12/29 11:37
結論は
 ソフトウェア工学を勉強してください
でよろしいか?

明らかに知識不足・経験不足な1。

43 :デフォルトの名無しさん:02/12/29 11:38
>>37 ソフトウェア工学の本ばかり読んでいて現場の泥臭い作業を知らなさそうな発言ですかい?
複雑にすれば、そのソースコードを見たものは皆いらいらする。
複雑にすればするほど欠陥は増えるだろが



44 :デフォルトの名無しさん:02/12/29 11:39
>>41
宿題は自分でやってください

45 :デフォルトの名無しさん:02/12/29 11:40
>>43
ジョークだろ…

46 :デフォルトの名無しさん:02/12/29 11:41
しかし、ここまで1がアレなスレも久々だな。

長期休暇ってこれだからいやだ

47 :デフォルトの名無しさん:02/12/29 11:42
>>38
そんな単純なものなら誰も苦労しません。

48 :デフォルトの名無しさん:02/12/29 11:42
>>43
おまいさんはもうすこし本を読んだほうがいいぞ。

49 :37:02/12/29 11:43
>>43
引用に反論するなよ(藁

50 :1 ◆o/H5.DRW4g :02/12/29 11:45
>38
正当性は参照透過性が確保されていれば証明できると思います。
副作用を使わないと限定的なプログラムしか書けそうにありませんが。

51 :デフォルトの名無しさん:02/12/29 11:48
まあ、1が最終的にいいたいのは.netを使えばメモリ関連のバグの大部分は
防げるから.netに移行しろ、ってことだよ。

52 :デフォルトの名無しさん:02/12/29 11:50
>35
http://mentai.2ch.net/test/read.cgi/infosys/958221505/l50
を読んで、電波を感じろ。

53 :デフォルトの名無しさん:02/12/29 11:51
ジッサクジッエン♥

54 :デフォルトの名無しさん:02/12/29 11:54
現実には有り得ない様な実験的な開発環境(人間関係とか、
生活環境とかも含む広義の定義で)を作れば不可能じゃないとは思うが、
現実にそんな開発体制を期待するのは意味がない。。。

>>1はそういう理想論を語りたいのか?


55 :デフォルトの名無しさん:02/12/29 11:55
ここから>>1に、どのソフトウェア工学の本を読めばいいのかを教えるスレに
なりました。

56 :デフォルトの名無しさん:02/12/29 11:56
現実が見えてない夢見がちな1に萌え

>>55
で、何がおすすめ?

57 :デフォルトの名無しさん:02/12/29 11:56
バグかどうかわからないプログラムを仕事で引き継いじゃったばあいはどうすればいいの?

58 :デフォルトの名無しさん:02/12/29 11:57
>>57
もらった時点でバグはない、と定義する。
バグリストがあれば別だが…

59 :デフォルトの名無しさん:02/12/29 11:58
おまえら、冬厨をあんまりいじめると荒らしに変わるぞ…

60 :デフォルトの名無しさん:02/12/29 11:59
>>57
他の奴に引き継げ

61 :デフォルトの名無しさん:02/12/29 12:00
>>58
もらった時点でバグはあると仮定して工数取っとく、だろうが。

62 :デフォルトの名無しさん:02/12/29 12:00
>>57
バグは無いと定義する?違うよJOJO。逆に考えるんだ。
バグっているに決まってるさと考えるんだ。

63 :デフォルトの名無しさん:02/12/29 12:01
>>1はどこへ行った〜?

64 :デフォルトの名無しさん:02/12/29 12:01
バグ取りで鬱になった患者がいるスレはここですか?

65 :1 ◆o/H5.DRW4g :02/12/29 12:02
>>63
>>52を読んでます。


66 :デフォルトの名無しさん:02/12/29 12:03
「いくつバグを出せば気が済むんだ?」
「おまえは潰したバグの数を覚えているのか?」

67 :デフォルトの名無しさん:02/12/29 12:04
          ☆ チン       
                       
  ☆ チン  〃  ∧_∧   / ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄
    ヽ ___\(\・∀・)< 削除依頼まだ〜?
        \_/⊂ ⊂_)_\____________
      / ̄ ̄ ̄ ̄ ̄ ̄ ̄/|
    |  ̄  ̄ ̄ ̄ ̄ ̄ ̄:| :|
    | 全日本クソスレ同盟|

68 :デフォルトの名無しさん:02/12/29 12:07
>>57 そのプログラムが気に入らなければ自分で作り直せ

69 :デフォルトの名無しさん:02/12/29 12:09
このスレは糞スレなんだね、兄貴!
兄貴の言うことが今!言葉でなく心で理解できた!
そして「削除依頼してやるッ!」と思ったときにはすでにッ!

依頼は終わっているんだね…。
http://qb.2ch.net/test/read.cgi/saku/1027372992/98

70 :デフォルトの名無しさん:02/12/29 12:10
ジョジョマニアがいる…

71 :デフォルトの名無しさん:02/12/29 12:17
>>69
削除理由が厳しいな

72 :デフォルトの名無しさん:02/12/29 12:19
削除願いをだして実際に削除されたスレを見たことが無いのは俺だけか?

73 :デフォルトの名無しさん:02/12/29 12:20
>>72
ageんな、ボケ!

74 :デフォルトの名無しさん:02/12/29 12:22
>>73
sageんな、ブァケ

75 :デフォルトの名無しさん:02/12/29 12:23
証明って、prologとか?

76 :デフォルトの名無しさん:02/12/29 12:30
>>1
一行目は何も実行しないプログラムを作ればバグがないので可能。

二行目は計算機停止問題と同等な問題。
よって前提に 「あらゆるプログラムに対して」 がつくならば不可能。

で、できることは、ある問題領域(特定の特徴を持つプログラム)の
特定の種類のバグがあるかないかを調べること。
配列境界、到達可能性(ガベレージ) あたりはコンパイラでもできている。

プログラムはあっているが仕様が正しくないというバグはどうやって見つける?

77 :デフォルトの名無しさん:02/12/29 12:33
>>76

> プログラムはあっているが仕様が正しくないというバグはどうやって見つける?

実務的には、こちらの方が重要。

78 :デフォルトの名無しさん:02/12/29 12:35
1は逃げました

79 :デフォルトの名無しさん:02/12/29 13:02
public Add {
 public addOne(int value) {
  value++;
  return value;
 }
}
public AddTester extends TestCase {
 public void testAddOne() {
  Add add = new Add();
  assertEquals(add.addOne(1), 2);
 }
}

80 :デフォルトの名無しさん:02/12/29 13:05
>>77
テストを書くといいよ。

81 :デフォルトの名無しさん:02/12/29 13:17
>>1
> バグが一切無いプログラムを作成することは可能か?
> また、「バグが一切無い」と証明する方法は存在するのか?

>>11
> 昔々、チューリングが、「そんな方法ねー」と証明しますた。

>>13
> それは知ってますが、だからと言って全く考えないのでは
> 知能の敗北でしょう。
> 別に「100%正しい」と証明する必要はありません。

(゚Д゚)ハァ??

82 :デフォルトの名無しさん:02/12/29 13:20
> 別に「100%正しい」と証明する必要はありません。
時間の無駄でしょう

83 :デフォルトの名無しさん:02/12/29 13:35
少なくとも、テストで目的地までの「道」を作ることは出来る。
踏み外したら無慈悲に警告して、バグが生まれたことを教えてくれる「道」だ。
警告が出ないようにプログラムを直せば、いまのところ仕様が
満たされていると安心できるような、そんな「道」だ。

ま、それをどう思うか--便利だと思うか、うっとおしいと思うか--は、
開発者の判断に依存するだろうが。

84 :デフォルトの名無しさん:02/12/29 13:44
人間が作るものにバグがないものなんて…

85 :デフォルトの名無しさん:02/12/29 13:44
>>11
> 昔々、チューリングが、「そんな方法ねー」と証明しますた。

それは「任意のプログラムについて」正しいかどうか判定するプログラムでしょ?
特定のプログラムに限定すればその限りではなかったはず。

86 :デフォルトの名無しさん:02/12/29 13:49
任意=すべて⊃特定

87 :デフォルトの名無しさん:02/12/29 14:13
バグ数 = 潜在バグ数/(意味のあるテストの数×実施頻度)

#ところで、プログラムのバグを見つけたら賞金を出すとか言ってた教授いなかったか?

88 :デフォルトの名無しさん:02/12/29 14:14
面白い命題だ。
一応、仕様は完璧でコンパイラも完璧という前提で話しあった方が
生産性があると思う。
プログラムが仕様通りに動かないとバグというわけだ。


89 :デフォルトの名無しさん:02/12/29 15:15
>>87
ディルバートのネタになったやつかな。
「では、車が買えるくらいのバグをこれから仕込みます」

90 :デフォルトの名無しさん:02/12/29 15:20
1.仕様書が要求する動作をテストする、テストコードを書く。
2.コンパイルが成功するような、実装コードを書く。
3.テストが成功するような、実装コードを書いてゆく。
4.実装コードが動く場合、期待どおりに動いているか、クライアントに見てもらう。
5.全てのテストが成功した場合、バグは無いと判断する。

これを改良してみたい。

91 :デフォルトの名無しさん:02/12/29 15:22
    ∧ ∧         / ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄
| ̄ ̄( ゚Д゚) ̄ ̄|   <  >>1が来るまで一眠りするからな!
|\⌒⌒⌒⌒⌒⌒\   \
|  \           \    ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄ ̄
\  |⌒⌒⌒⌒⌒⌒|
  \ |_______|

92 :デフォルトの名無しさん:02/12/29 15:33
#include <iostream>
#include <cstdlib>

int main()
{
 std::cout<<"俺のチンコはぬるぽ"<<std::endl;
 return EXIT_SUCCESS;
}

//移植性も良く
//正しいヘッダもincludeされていて
//しかもバグも無い
// 完 璧 !

93 :デフォルトの名無しさん:02/12/29 16:10
>>92
短いプログラムならバグのない完璧なプログラムは可能なはず。
しかし、コードが段々増えていくと、混沌としてくる。

94 :デフォルトの名無しさん:02/12/29 16:14
>>92
完璧ではない。
出力してる文字列が意味不明。

95 :デフォルトの名無しさん:02/12/29 16:22
テストを基本に「バグの無さ」の確証度をはかるのなら、
せめてテストカバレッジぐらいは押えてくれ。

あとテストに拘らないのなら、
せめて誰か表示的意味論という名前ぐらい出してやれ。

96 :デフォルトの名無しさん:02/12/29 17:04
ま、1 には何も期待しない方がいいな。

97 :デフォルトの名無しさん:02/12/29 17:24
結局ケツまくって逃げたんか、1は。
来るとしても「寝てました」「出かけてました」「資料読んでました」

厨房氏ね

98 :デフォルトの名無しさん:02/12/29 19:19
だからバグってのはなにを指しているんだよ。
意図した処理と違っていてもバグだろーが。
別にメモリ破壊して暴走した、とかだけがバグじゃねーだろーに。
メモリ関連のバグってことだけなら十分防ぎようはある。


99 :デフォルトの名無しさん:02/12/29 19:23
>>1
自分の愚かさに気が付きましたか?
それなら早めに削除依頼を。

100 :デフォルトの名無しさん:02/12/29 19:25
>>99
一応もう出てるぞ。

101 :デフォルトの名無しさん:02/12/29 19:27
完璧なプログラムとは、未来永劫にわたって
修正・仕様拡張のない完璧な安定性と機能を兼ね備えたプログラムのことだ。


102 :デフォルトの名無しさん:02/12/29 19:30
>>101
修正と仕様拡張を同じと考えているアホ発見

103 :デフォルトの名無しさん:02/12/29 19:36
>>102
同じじゃないから分けて書いたんだろ。アフォが。
漢字ドリルの宿題はちゃんと終わったのか?

104 :デフォルトの名無しさん:02/12/29 19:42
>>103
恥ずかしい奴。「修正・仕様拡張」って書き方は同じ物としてみなす書き方なんだよ。
覚えときな。

105 :デフォルトの名無しさん:02/12/29 19:50
バグがあっても契約期間がすぐ終わるので、見てみぬふりをしたんですが、
誰も気づいてないバグはバグなんですか?

106 :デフォルトの名無しさん:02/12/29 19:53
>>105
そのプログラムがお役目御免になって破棄されるまでにだれにも気づかれなければバグではありません。


107 :デフォルトの名無しさん:02/12/30 02:20
逃げた1を晒しあげ

108 :デフォルトの名無しさん:02/12/30 05:09
いくらでも研究例があるのですが。
http://www.google.com/search?q=software+verification&hl=ja&num=50

109 :デフォルトの名無しさん:02/12/30 12:55
>>108
そういうモノをかみ砕いて要約して書込んでもらえれば有意義なのですが、
ただ検索結果を貼られても困る。


110 :名無しさん@Emacs:02/12/30 13:07
>>87,89
それって TeX じゃないの?

111 :デフォルトの名無しさん:02/12/30 13:13
>87
djbと言ってみる。

112 :デフォルトの名無しさん:02/12/30 13:25
「欠陥ゼロのソフトウェア開発」(日経BP)

積読。
鬱だ。

113 :デフォルトの名無しさん:02/12/30 13:27
>>109
自分では検索すらしないくせに他人に対する要求だけはエラそうに一人前ですか。
(人格に欠陥があるのでは?)

114 :デフォルトの名無しさん:02/12/30 14:51
>(人格に欠陥があるのでは?)

はい、2ちゃんねら自体そうです;-)

115 :デフォルトの名無しさん:02/12/30 15:01
>>113 スゲーナおめー、検索が出来るのか。
俺はまだまだ初心者だから、検索って何かわからなくて途方に暮れてたんだ。
検索した結果を貼ってくれてありがとう!あそこの四角の所にキーワードを入れるのかぁ、なるほど〜。

116 :デフォルトの名無しさん:02/12/30 15:12
>>108
その青い下線のところの記号の意味がわかりません。

117 :デフォルトの名無しさん:02/12/30 15:30
>>116 スゲーナおめー、青が分かるのか。
俺はまだまだ初心者だから、青って何かわからなくて途方に暮れてたんだ。

118 :デフォルトの名無しさん:02/12/30 15:56
初心者は免罪符ではありませーん

119 :デフォルトの名無しさん:02/12/30 15:59
>>118 スゲーナおめー、初心者が分かるのか。
俺はまだまだ初心者だから、初心者って何かわからなくて途方に暮れてたんだ。

120 :デフォルトの名無しさん:02/12/30 15:59
http://dictionary.goo.ne.jp/cgi-bin/dict_search.cgi?MT=%CC%C8%BA%E1%C9%E4&sw=2

121 :デフォルトの名無しさん:02/12/30 16:01
すげーな109。
粘着のきわみだな。

122 :デフォルトの名無しさん:02/12/30 16:03
なにをもって、完璧なのかが問題だ

123 :デフォルトの名無しさん:02/12/30 16:05
現在のOS用のプログラムは全部バグ付き

124 :デフォルトの名無しさん:02/12/30 16:07
>>121 スゲーナおめー、粘着が分かるのか。
俺はまだまだ初心者だから、粘着って何かわからなくて途方に暮れてたんだ。

125 :デフォルトの名無しさん:02/12/30 16:09
>>124
そのコピペ、流行ってるの?

126 :デフォルトの名無しさん:02/12/30 16:15
まじで?

127 :デフォルトの名無しさん:02/12/30 16:48
それはギャグで言っているのか?

128 :デフォルトの名無しさん:02/12/30 17:26
スゲーナおめー、ギャグが分かるのか。
俺はまだまだ初心者だから、ギャグって何かわからなくて途方に暮れてたんだ。

129 :108:02/12/30 17:35
はいはい、じゃあさらっと解説してやるよ。
オレも大学の授業でかじっただけなんで詳しくは知らないよ。

ソフトウエア検証は表示意味論 (denotational semantics) にもとづいている。
早い話がプログラムの仕様と動作をぜんぶ数学に落とすのだ。
そうすればプログラムの正当性は数学的な証明でできる。
よくある例が、以下のコードが n! をきちんと計算することを証明するというやつ。

i=1; x=1;
while (i<n) {
 i=i+1; x=x*i;
}
return x;


130 :108:02/12/30 17:37
ここでプログラムの実行中を通してつねに変わらない条件式を考える。
これは不変式 (invariant) と呼ばれる。ここでは x == i! を選んだ。
つぎにこの式が各ステップでつねに成りたつことを示す。
ループ中では数学的帰納法と似たような仮定をつかって、
「ここで成りたっていると仮定すると、次のステップでも成りたつ」と証明する。
そしてプログラムの各行ごとに証明を書いていく。

i=1; x=1;
/* この時点で 1 == 1! なので x == i! が成りたっている */
while (i<n) {
 /* まず、この時点で x == i! が成りたっていると仮定する */
 i=i+1; x=x*i;
 /* この時点で新しい x と i をそれぞれ x'、i' とすると、
  x' = (x*(i+1)) == i!*(i+1) == (i+1)! == i'! なので、
  新しい x' と i' についても x' == i' が成りたつ */
}
/* ループが終了した時点で、while の条件は否定されているはずだから
  ここでは !(i<n) すなわち i>=n がなりたっているはずである。
  さらにここでも x==i! が成りたっているので、 x>=n! */
return x;

131 :108:02/12/30 17:37
これで x が最終的に n! 以上にあることが証明された。
厳密にイコールであるとはいえなかったけど、概略はこんな感じ。
もし while の条件が (i<=n) だったら、ループが終了したときには i>n となり、
x > n! になってしまうので間違いだとわかる。
i=i+1; と x=x*i; の順番を変えても不変式が成りたたなくなるので、
間違いだとわかるだろう。
こういうことを実際にプログラムを実行せずに論理的に答えられる。
これがソフトウエア検証という技術。

ただし、この方法は仕様が数式できっちり表現できるようなプログラムにしか
使えない。でもたいていのプログラムは数式ですべてを表現するには複雑すぎる。
これをいかに簡単にするか、というのが現在のソフトウエア検証論の研究。


132 :デフォルトの名無しさん:02/12/30 17:46
ということにしたいんですね:P

133 :133:02/12/30 18:02
そうですよ:-b

134 :デフォルトの名無しさん:02/12/30 18:05
今更ぺこちゃんスマイルかよ。

135 :デフォルトの名無しさん:02/12/30 19:17
極論言ったら世界には何も証明できることはないことになるぞ

136 :デフォルトの名無しさん:02/12/30 22:06
>>135
証明できることはない、を証明してみろよ(藁

137 :デフォルトの名無しさん:02/12/31 06:45
>>136
自己矛盾してるよ(藁

138 :デフォルトの名無しさん:02/12/31 13:52
>130
で、char x;という落ちが付く。

139 :デフォルトの名無しさん:02/12/31 23:49
ここの議論には誰も期待してなさそうだな。
定義しろ厨が跋扈してるし。
俺が定義してやる。

そうだな...


140 :デフォルトの名無しさん:03/01/05 15:56
完璧な駄スレ

141 :デフォルトの名無しさん:03/01/05 16:35
完璧な涙

142 :デフォルトの名無しさん:03/01/07 09:52
>>141
他人のバグを見付けたPG
 「君のために泣く」

143 :IP記録実験:03/01/08 21:53
IP記録実験
http://qb.2ch.net/test/read.cgi/accuse/1042013605/

1 名前:ひろゆき ◆3SHRUNYAXA @どうやら管理人 ★ 投稿日:03/01/08 17:13 ID:???
そんなわけで、qbサーバでIPの記録実験をはじめましたー。

27 名前:心得をよく読みましょう 投稿日:03/01/08 17:20 ID:yL/kYdMc
SETTING.TXT管轄でないということは全鯖導入を視野に、か?

38 名前:ひろゆき ◆3SHRUNYAXA 投稿日:03/01/08 17:22 ID:rLfxQ17l
>>27
鋭いです。

73 名前:ひろゆき ◆3SHRUNYAXA 投稿日:03/01/08 17:27 ID:rLfxQ17l
>ところで、IPが抜かれて何か今までと変わることってあるのでしょうか?
・今までより、サーバが重くなる。
・裁判所や警察からの照会があった場合にはIPを提出することがある。

144 :デフォルトの名無しさん:03/01/09 01:39
>>352
ほんまですか?

145 :デフォルトの名無しさん:03/01/09 03:11
各板「のトップに「当インターネットはフィクションであり・・・・」ってのせとけばそれで良くない?

146 :デフォルトの名無しさん:03/01/09 03:56
つか、自宅鯖に掲示板を置かなくても、串入れてログとらないようにして、
「知らない間にハカーが侵入して勝手に串を立てられたんです」
ということにしておけば十分神になれるか。

147 :デフォルトの名無しさん:03/01/09 13:09
http://qb.2ch.net/test/read.cgi/accuse/1042013605/352

148 :デフォルトの名無しさん:03/01/09 13:10
>>146
業務上過失

149 :デフォルトの名無しさん:03/01/09 14:56
記念パピコ

150 :デフォルトの名無しさん:03/01/09 17:25
======2==C==H======================================================

         2ちゃんねるのお勧めな話題と
     ネットでの面白い出来事を配送したいと思ってます。。。

===============================読者数: 138720人 発行日:2003/1/9

年末年始ボケがそろそろ収まり始めた今日このごろのひろゆきです。

そんなわけで、年末に予告したIP記録ですが実験を開始しています。

「2ちゃんねる20030107」
こんな感じで各掲示板の最下部に日付が入ってるんですが、
20030107以降になってるところはログ記録実験中ですー。

んじゃ!

────────────────────────Age2ch─
■この書き込みは、Age2chを使って配信されています。
────────────────────────────
Keep your thread alive !
http://pc3.2ch.net/test/read.cgi/software/1041952901/l50
────────────────────────────

151 :デフォルトの名無しさん:03/01/09 23:15
此れで皆実質「名無し」では無くなる訳だが

152 :デフォルトの名無しさん:03/01/10 09:42
おやすみ。最近風邪が流行ってるから大事にな〜>けんすう

153 :デフォルトの名無しさん:03/01/10 10:03
おやすみ。最近風邪が流行ってるから大事にな〜>けんすう

154 :デフォルトの名無しさん:03/01/10 10:22
根本的におもしろくなけりゃ乗ることもできないわけで、、

155 :デフォルトの名無しさん:03/01/10 10:54
こんなんが立て続けに起きれば、ひろゆき破産→夜逃げ。
あっという間に2ch閉鎖だな。

逆に、現在のように放置せず、きちんと管理するとなれば経費が掛かるし、
利用者が離れていく事に。

どうする?ひろゆき。

156 :デフォルトの名無しさん:03/01/10 11:38
やったね。


157 :デフォルトの名無しさん:03/01/10 12:06
とりあえずbbs.cgiを止めてくれ。

158 :デフォルトの名無しさん:03/01/10 12:56
567が良い事言った          

159 :デフォルトの名無しさん:03/01/10 15:21
あわわ、キャップつけたまま送信しちゃった。。ごめんなさい。

160 :デフォルトの名無しさん:03/01/10 16:49
気球がとんできましたスレどこー?

161 :デフォルトの名無しさん:03/01/10 23:14
ところで、アホーの投票祭り無いの?
俺は「2ちゃんねるってなに?」に投票してきたけど。

162 :デフォルトの名無しさん:03/01/11 00:32
俺は晒す自身がないな。。。

163 :デフォルトの名無しさん:03/01/11 00:40
言っとくけど禿げしく既出。

164 :デフォルトの名無しさん:03/01/11 10:03
>WINNYなんて、倒産・違法化したら結局存在できない訳でしょ。
WINNY倒産・・・








                               笑うとこ?

165 :デフォルトの名無しさん:03/01/11 10:36
======2==C==H======================================================

         2ちゃんねるのお勧めな話題と
     ネットでの面白い出来事を配送したいと思ってます。。。

===============================読者数: 139038人 発行日:2003/1/10

なにやら、連日メルマガだしてるひろゆきです。

そんなわけで、ログ記録実験ですが、いちいちサーバ指定するのが面倒なので、
全部のサーバに入れてみました。

重くなって落ちたりしてもご愛嬌ってことで。。。

んじゃ!

────────────────────────Age2ch─
■この書き込みは、Age2chを使って配信されています。
────────────────────────────
Keep your thread alive !
http://pc3.2ch.net/test/read.cgi/software/1041952901/l50
────────────────────────────

166 :デフォルトの名無しさん:03/01/11 12:00
はー

167 :デフォルトの名無しさん:03/01/11 13:04
(いや、馬鹿に馬鹿といっても侮辱罪止まりなんですが・・・とマジレス)

168 :デフォルトの名無しさん:03/01/11 13:33
削除しなかったことが問題であって、IP取得は全くの見当違いだと思うんだが
それよかズボラな削除体制どーにかしろって感じだな

どさくさに紛れて都合の良い法律案を盛りこむ議会みたい
管理批判の多い板から記録してるっつーのもなんだかなあ

169 :デフォルトの名無しさん:03/01/11 16:18
電波を演じてるのか、ほんものの電波なのか・・・
400レス以上演技は続かないかな・・・

170 :デフォルトの名無しさん:03/01/11 16:25
鳴る歩道って。
ログのリンクが無い時点で
信憑性なんかほとんどゼロだろ。

171 :デフォルトの名無しさん:03/01/12 00:28
IP記録スレは有るよ

IP記録実験2
http://news2.2ch.net/test/read.cgi/newsplus/1042030554/


172 :デフォルトの名無しさん:03/01/12 00:38
コストかけるといけないの?(^_^;)

さあ?(^_^;)

173 :デフォルトの名無しさん:03/01/12 03:15
(・∀・)?

174 :デフォルトの名無しさん:03/01/12 03:17
ピー


      し ば ら く お ま ち く だ さ い




  

175 :デフォルトの名無しさん:03/01/12 10:47
初めて立てた・・・・(;´Д`)

176 :デフォルトの名無しさん:03/01/12 21:22
12/24
    |                   \
    |  ('A`)           ギシギシ
   / ̄ノ( ヘヘ ̄ ̄        アンアン/

12/25
    |                   \
    |  ('A`)           ギシギシ
   / ̄ノ( ヘヘ ̄ ̄        アンアン/

1/1
    |                   \
    |  ('A`)           ギシギシ
   / ̄ノ( ヘヘ ̄ ̄        アンアン/



177 :デフォルトの名無しさん:03/01/12 21:25
それはそのとおりだが、実際問題としては、そこまで追っかける人は少ないようだよ。

178 :デフォルトの名無しさん:03/01/12 21:36
大変よいところに気付きました。

そう言う風にダラダラした負荷が続くときは、
鯖のリブートが必要なのです。
更にこの現象が悪化するときは、夜勤さんを召還してください。

やりかたはこう。
夜勤さん!! ヘ(^^ヘ)(ノ^^)ノ


179 :山崎渉:03/01/13 18:59
(^^)

180 :デフォルトの名無しさん:03/01/13 23:26
さーど じゃなくて さんど だろ。

181 :山崎渉:03/01/15 18:13
(^^)

182 :デフォルトの名無しさん:03/01/20 23:53
通報しますた

183 :デフォルトの名無しさん:03/01/20 23:55
Hoo!Hoo!

184 :山崎渉:03/01/23 20:06
(^^)

38 KB
■ このスレッドは過去ログ倉庫に格納されています

★スマホ版★ 掲示板に戻る 全部 前100 次100 最新50

read.cgi ver 05.02.02 2014/06/23 Mango Mangüé ★
FOX ★ DSO(Dynamic Shared Object)