Coq and Why : Formal Verification Tools
MPAなWebフレームワーク、Astroの紹介 (その2) 2024/05/24の勉強会で発表されたものです。
みずほ銀障害に見る、人災と人為ミスの違い
みずほ銀行が3月に引き起こした大規模システム障害は、東日本大震災の義援金が引き起こした「天災」ではなく、明らかに「人災」だ。しかもシステム障害の原因は、現場の担当者の不手際といった人為ミスにあるのではなく、経営陣のITガバナンスの欠如にある。同行が5月に発表した調査報告書（pdf）が、そのことをはっきりと物語っている。 日経コンピュータでは6月9日号で、みずほ銀行が第三者委員会「システム障害特別調査委員会」に依頼して作成した調査報告書を独自に読み解き、分析した。その結果、みずほ銀行のシステム障害は、30の「不手際」が積み重なることで長期化したことが分かった（表）。 30の不手際の詳細は、日経コンピュータ6月9日号の「緊急特集」としてまとめたほか、同記事は6月13日から1週間に分けてITproにも転載する予定である。みずほ銀行のシステム部門が、多くの人為ミスを犯したのは事実だ。混乱のさなか、
一歩先行くJavaプログラマが読むべきオープンソースソフトウェア10選 - 設計と実装の狭間で。
10万行コード読んだらJava分かるよってTwitterに書いたらすげぇ勢いでRTされたので、調子に乗って捕捉エントリ書くよ。 Java Core API JDKインストールしたディレクトリに入ってるsrc.zipを展開すると入ってるから読むと良いよ。 すぐ近くにあるのから読むってのはメンタル的に楽でいい。 厳密にはOSSじゃなくて単に公開されてるってだけなんだけども、JavaプログラマなのにコアAPIのコード読んでないとか無いよね？ どれから読めば良いか分からんかったら、 java.lang java.util java.io java.text 辺りをまずはキチンと理解すること。当然コードを読み終わったら、それを使ってコードを書く事。 OpenJDK http://hg.openjdk.java.net/jdk7/jdk7 OpenJDKを読むことで、プログラム言語してのJavaではな
期待のiOS 5で、どこまで世界は変わる？ 200を超える新機能を厳選徹底解説！
期待のiOS 5で、どこまで世界は変わる？ 200を超える新機能を厳選徹底解説！2011.06.09 18:00 これは本当に待ち遠しい！ 新たなる｢iPhone 4S｣または｢iPhone 5｣のハードウェアのお披露目こそありませんでしたが、iPhone、iPod touch、iPad向けに今秋にリリースされる新｢iOS 5｣には、数々の感動と興奮をもたらしてくれそうな発表も目白押しでしたよね。いまからワクドキしちゃってるギズ読者の皆さまも多いのでは？ WWDC 2011では、この期待のiOS 5の中でも10大新機能に絞って紹介発表が行なわれていましたが、でも、実際のところは、iOS 5で追加される機能って200を超える盛りだくさんなラインナップなんですよねぇ。さすがにすべてを紹介しきることはできませんけど、おさらいも含めまして、大きくモバイルシーンに変化をもたらしてくれそうな、iOS
形式仕様記述 - Wikipedia
形式仕様記述（けいしきしようきじゅつ、英: formal specification）とは形式手法のひとつで、何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述である。 形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる(形式的検証)。また、仕様策定の工程で仕様の不整合を検出することが可能となり、実装工程のような開発の後半での仕様不備発覚、それに伴う手戻り(多大なコストを要する場合が多い)を防ぐという利点がある。他の使われ方として、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化し、開発工程で不具合を作りこむのを防ぐ。 設計（や実装）の「正当性」はそれ自身だけで確認できないという点が重要である。正当性は与えられた仕様に照らして初めて検証可能であり、形式仕様記述
いまさら聞けない 形式手法入門
ソフトウェアの品質向上手段として注目されている形式手法。今回は、厳密な仕様定義を目的とした「形式仕様記述」を中心に、分かりやすく解説する ソフトウェアの品質を確保するため、誰もがレビューとテストを行います。しかし、一般的に行われているレビューやテストにおいて、システムが正しく動作することをどの程度保証できているのでしょうか。優秀なエンジニアによる小規模ソフトウェア開発であれば、設計・テスト・検証における細心の注意とノウハウにより高品質のシステムを実現することが可能です。では、50人を超えるようなチームではどうでしょうか。 ここでは、ソフトウェアの品質と安全性向上のために、「プログラムの正しさ」に関する研究から生まれた「形式手法（Formal Method）」を簡単に紹介します。 形式手法とは 形式手法とは、1970年代から始められたプログラム開発手法の1つで、論理学や離散数学などが基礎にな
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Formal methods20100529
エンジニア・ミーツ・Coq プラスワン
Login | Microsoft 365