サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
都知事選
masateruk.hatenablog.com
本記事は、形式検証 / 形式手法 Advent Calendar 2021 の 19 日目の記事です。 Amazon S3が形式手法を採用した論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" を読みました。 論文全体については、yohei-aさんがブログ記事で主要な部分を訳してくれています。本記事では自分なりのまとめに加えて、自分の形式手法導入の経験から思うところについても書いてみます。 論文は、Amazon S3の新しいKey ValueストレージのShardStoreの正当性を軽量形式手法で検証した話です。論文の主張をまとめると、 実装に使用した言語(Rust)と同じ言語で仕様となるリファレンスモデルを記述した。 検証したい性質によってツールを使い分けた。機能的
AWSにおける形式手法の記事(https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf)を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる 以下は、読んでいる途中で書きだした要点。 AWSでは2011年以降形式仕様とモデル検査を使用している 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレス
私は5年ほど前から、仕事に費やす時間を計測している。何に、何分費やしたか?をすべて記録している。その記録を見返せば何時何分には何をやっていたのかを知る事ができる。私がこのような計測をしているにはねらいがあって、それは、 計測データを蓄積する事で、そのデータをもとにより正確な見積もりができるようになる 何に、何分かけているのかを見て反省する事でより効率的なプロセスを発見する である。 さて、5年やった実績から先に言うと、残念ながらどちらも達成できていない。1 に関してはたまに見積もりのデータとして活用することはあるが、その結果どのくらい正確だったかはわからないし、2 についてはまったく効率的なプロセスの発見には至っていない(どころか発見の助けにもなっていない)。 なぜ上記ねらいが達成できてい理由は2つあげられる。ひとつは、 a. 仕事の内容が過去と同じではない である。ソフトウェア開発という
後輩に形式手法を学び始めたときに読んだ本を紹介すると約束したので、せっかくなのでブログに書くことにした。 形式手法を学び始めたのは2004年だから、今から始める場合はまた違ったラインナップになるだろうけど。 ※「2012年に形式手法を学び始めるならこの7冊 - masaterukの日記」を書きました。 1冊目。 プログラミングの科学 (情報処理シリーズ) 作者: D.グリース,筧捷彦出版社/メーカー: 培風館発売日: 1991/01メディア: 単行本 クリック: 20回この商品を含むブログを見る出会いはこの本。僕の人生を変えてしまった本だ。この本に出会ったときの衝撃は今でも覚えている。命題と述語からはじまり、ホーア論理、そしてプログラムの作り方が解説してある。「プログラムの作り方」を解説している本は少ない。Twitterでもつぶやいたけど、assertの使い方を教えてくれたのもこの本だった
OCamlで書いてC言語に変換するプログラム、最低限入れたかった機能を実装して一応形になりました(ソースコードはこちら)。プライベートな時間をちまちま使って作ったので思ったより時間がかかってしまいました。最初にブログで紹介してから1年半もたちました。 OCamlをC言語に変換するプログラムをつくりました - masaterukの日記 サポートしている基本型は、Int型とBool型のみ。レコード型とバリアント型も使えます。型変数による多相型も定義できます。リスト型だけ組み込みでサポートしました(ただしライブラリはありません)。 関数を定義するときには、再帰関数でなくてもlet recとするのはMinCamlと同様です。ラムダは書けませんが、クロージャはサポートしてます。matchによるパターンマッチをサポートしているので、だいぶ書けるものが増えました。 たとえば、Haskellの例でよく引き
この記事は TDD Advent Calendar 2012 の最終日の記事です。前日の記事は@biacさんの「[コラム] テストファーストとは何か?: TDD.NET」、初日の記事は@sue445さんの「Try Dream Development : 夢の開発を始めよう #TddAdventJp - くりにっき」です。 TDD Advent Calendarの記事なのですが、TDDというより単体テストの話です。単体テストのやり方について人それぞれやり方があるかと思いますが、自分が単体テストをするときの手順をまとめてみました。以下がその手順です。 テストするメソッドを決める。 メソッドの仕様を確認する。 事前条件をいくつかに場合分けする。 上で分けた場合ごとに、テストケース用のメソッドをつくる。 テスト対象のクラスのインスタンスを生成し、場合分けしたひとつの事前条件を満たすコードを追加する
前エントリー「僕が形式手法を学び始めたときに読んだ10冊 - masaterukの日記」のラインナップはあまりに入手困難なものばかりだったので、2012年に始めるならということで改めて選んでみた。 1冊目。 VDM++によるオブジェクト指向システムの高品質設計と検証 (IT architects’ archive) 作者: ジョン・フィッツジェラルド、ピーター・ゴルム・ラーセン、ポール・マッカージー、ニコ・プラット、マーセル・バーホフ,酒匂寛出版社/メーカー: 翔泳社発売日: 2010/08/03メディア: 大型本購入: 1人 クリック: 32回この商品を含むブログ (8件) を見るVDM++の本。形式手法を学び始めるならこの本から始めると取っ付きやすいのではないかと思う。高級言語をつかった陽関数定義(実行可能形式)でモデルをがんがん書いて、シミュレーションとテストでモデルを洗練していくや
MinCamlをベースにしてOCamlをC言語に変換するプログラムをつくりました。 https://github.com/masateruk/micro-caml 何でそんなものをつくったかと言うと、わたしは組み込みプログラムの開発を仕事にしているのですが、 自分はOCamlで開発したい(C言語の型検査は心もとない。OCamlの強力な型検査に守られてコードを書きたい) しかし、OCamlで書くと誰も引き継げないため、使わせてもらえない。 ということで、自分が書くときはOCamlで書いて、納品するときにCに変換すればいいんじゃないかと思った次第です。OCamlを書ける人がいるんだったらOCamlのコードを引き継いでもらえばいいけど、Cしかわかりませんな人には変換後のCのコードを渡すという作戦です。もちろん、変換後のCのコードを直接変更しちゃうとOCamlのコードは役に立たなくなるんですけど、
とあることがきっかけで、コマンドキューをもつシステムをAlloyでモデル化し検証したので、ここで紹介します。 問題 あるシステムのミドルウェアを修正することになりました。このミドルウェアは整数値をやり取りするオブジェクトを複数所有します。インタフェースは以下の通りです。 assign(v) // オブジェクトの値をvに上書きします。 copy(obj) // オブジェクトobjの値をコピーします。 getValue() // オブジェクトの値を取得します。 このミドルウェアを実装するためにライブラリを使用しています。このライブラリはオブジェクトを複数所有しています。各オブジェクトはキューを持ち、コマンドをキューに積んでから実行する必要があります。コマンドは2種類あります。 assign(v)コマンドは、値の上書きする。 copy(obj)コマンドは、オブジェクトobjの値をコピー
このページを最初にブックマークしてみませんか?
『masateruk’s blog』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く