#TPP2014 高信頼な理論と実装のための定理証明および定理証明器

研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む
2
前へ 1 2 3 ・・ 6 次へ
Takashi Miyamoto @tmiya_

Ph.D 持ちを 100人規模で集めて大規模開発をやってみた、みたいな事例発表が聞いてみたい。大規模開発というと低いレベルに合わせるみたいな話しか耳にしないが。 #tpp2014

2014-12-04 10:53:57
おく @OKU_K

「国語」の問題と「数学」の問題 国語の問題の例 - 書式や用語や前提知識が読者と合意されている - 文法や語法や表記が正しい - 全体として読みやすく一貫性を持っている 「数学」の問題の例 略 #TPP2014

2014-12-04 10:56:14
Masahiro Sakai @masahiro_sakai

@tmiya_ Googleでの開発とか、そういうのありそうだけど、どうなんだろう。 #tpp2014

2014-12-04 11:00:40
おく @OKU_K

何のための「ソフトウェア工学」なのか ・人(開発メンバー)が死なないプロジェクト #TPP2014

2014-12-04 11:03:13
おく @OKU_K

おサイフケータイついてます #TPP2014

2014-12-04 11:05:13
おく @OKU_K

現場にプレッシャーをかけても品質は良くならずストレスばかりたまる #TPP2014

2014-12-04 11:09:01
おく @OKU_K

他には ・ホワイトボード ・独自仕様 ・UML ・自然言語 ・VDM #TPP2014

2014-12-04 11:12:57
おく @OKU_K

・ソフトウェアの開発現場では、曖昧な仕様に起因するトラブルが多い ・下流工程の修正コストは上流工程の10^n倍になる ・正しくないプログラムの血管修正は非常に難しい、または(基準点が無いため)不可能である #TPP2014

2014-12-04 11:15:17
おく @OKU_K

・自然言語により曖昧かつ不完全な仕様を記述している ・仕様記述と称して,手続き的日本語プログラミングを行っている #TPP2014

2014-12-04 11:15:36
Yoshihiro Imai @yoshihiro503

「SONYでは昔は新人はプログラム書いたりテストを書いたりしていたが、2000年くらいからすぐに仕様を書かされるようになった」 #tpp2014

2014-12-04 11:19:46
おく @OKU_K

・正しい使用を自然言語で書くのは困難である(形式仕様記述言語を用いても困難である) ・曖昧さの排除が困難 ・ツールに寄るチェックが出来ない ・仕様を書きながら「擬似コード」を考えなければならないことが多くなるが、文法の検討に時間がかる #TPP2014

2014-12-04 11:20:01
おく @OKU_K

・図表のレイアウト検討や記述にも時間がかかる ・変更管理が困難である ・改善方法やその基準がわからない…(仕様書がメンテ出来ない、されない…) ・仕様っぽいものが誰にでも書けてしまう… #TPP2014

2014-12-04 11:20:12
おく @OKU_K

日本語と英語ができる(&院卒)というだけで仕様記述を任される… #TPP2014

2014-12-04 11:22:12
おく @OKU_K

VDMによる仕様記述が10万行… #TPP2014

2014-12-04 11:24:38
Masahiro Sakai @masahiro_sakai

@Alcor80UMa @違ったので再投稿:たしかWhyのグループは、verificationのために形式的仕様が必要だが、現場のエンジニアが書いてくれないという問題に対し、形式的仕様からのテストケース生成を現場にも分かりやすいご利益/入口にしようとしてたはず #TPP2014

2014-12-04 11:32:07
Sosuke MORIGUCHI @chiguri

仕様10万行と実装11万行が今は15万行と38万行・・・ #TPP2014

2014-12-04 11:33:05
Yoshihiro Imai @yoshihiro503

「orとxorの違いもわからない人が仕様を書くべきではない。今はパワポがちょっとできるくらいの人が書いていてそれはちょっとよくない」 #tpp2014

2014-12-04 11:40:14
T.T. @t_teruya

VDM++から直接は生成していないけど,それは実装時に判断すべきことがあるから… それは現実的な判断だとは思う #TPP2014

2014-12-04 11:43:07
Sosuke MORIGUCHI @chiguri

Q:どうやってVDMを使うことについて上の方を説得した? A:別の会社ができたことによって責任の所在が明らかになり、またその会社が品質を必要としていたので得に反対はされなかった。 #TPP2014

2014-12-04 11:45:31
farvel @farvel

仕組みを作る/仕様書を書く人は数学力大事 - #TPP2014 高信頼な理論と実装のための定理証明および定理証明器 - Togetterまとめ togetter.com/li/753501 via @togetter_jp

2014-12-04 11:47:41
さかばー @saka_bar

#TPP2014 スライドって公開されているんですかね

2014-12-04 11:57:14
Takuma SHIRAISHI @ts7i

…。「仕様記述と称して,手続き的日本語プログラミングを行っている」『#TPP2014 高信頼な理論と実装のための定理証明および定理証明器』 togetter.com/li/753501

2014-12-04 12:16:28
Sosuke MORIGUCHI @chiguri

仕様を定義とすることで機能を理解するときに読む範囲が減る? #TPP2014

2014-12-04 13:13:00
Sosuke MORIGUCHI @chiguri

Fiat:プログラム導出フレームワーク。 プログラムを段階的詳細化によって合成する。 #TPP2014

2014-12-04 13:15:24
前へ 1 2 3 ・・ 6 次へ