[B! Formal-Method] masa8aurumのブックマーク

ゼロから学んだ形式手法 - DeNA Testing Blog

2020年1月に入社し、SWETの仕様分析サポートチームに加わったtakasek︵@takasek︶です。仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています︵形式手法カテゴリーの記事一覧︶。この記事では、加入3か月を経てようやく形式手法の輪郭が掴めてきた私の視点から、学習前後での理解の変化について振り返ります。想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。形式手法を学ぶ前の認識と疑問ソフトウェアエンジニアとしての私の一番の興味関心は設計手法です。設計は、なんらかの解決したい問題に対して、ある一面を切り取った構造︵モデル︶を与え、そのモデルを解決の機構に落

masa8aurum 2023/04/25

リンク

「せっかく記号を使った形式手法があるのに自然言語に戻るのか」というツイート - tkgshn

それはそうと、軽量な形式手法たる型システム含む形式手法は記号の世界の中での正気はちゃんと証明してくれるが、人間様が頭を捻って作られた、自然言語で書かれた仕様とやらは一体何の正気を保証してくれるんだろう

masa8aurum 2023/03/29

リンク

Software Abstraction 翻訳本のレビュワー募集 - まめめも

Alloy とかいう形式仕様記述言語があります。ソフトウェアの仕様を形式的に記述して検証とかして、上流設計をうまいことこなしちゃおう、とかいうアレです。で、Alloy の教科書とされる﹁Software Abstractions: Logic, Language, and Analysis﹂という本があります。 Software Abstractions: Logic, Language, and Analysisposted with amazlet at 11.02.09Daniel Jackson The MIT Press 売り上げランキング: 28680 Amazon.co.jp で詳細を見る ↑ここぞとばかりにアフィリエイト入ってみた。みんな絶対買うなよ！で、最近この本の翻訳に関わってました。bonotake さんや masahiro_sakai さんのお手伝い的な感じに。

masa8aurum 2021/11/20

形式手法の Alloy について

リンク

自動テストに限界を感じた私がなぜ形式手法に魅了されたのか - 若くない何かの悩み

長らく自動テストとテスト容易設計を生業としてきましたが、最近は色々な限界を感じて形式手法に取り組んでいます。この記事では、既存の自動テストのどこに限界を感じてなぜ形式手法が必要なのかの私見を説明します。なお、私もまだ完全理解には程遠いため間違いがあるかもしれません。ご指摘やご意見はぜひ Kuniwak までいただけると嬉しいです。著者についてプログラマです。開発プロセスをよくするための自発的な自動テストを支援する仕事をしています（経歴）。ここ一年は R&D 的な位置付けで形式手法もやっています。自動テストの限界自動テストとは私がここ数年悩んでいたことは、iOS や Web アプリなどのモデル層のバグを従来の自動テストで見つけられないことでした。ただ、いきなりこの話で始めると理解しづらいと思うので簡単な例から出発します。この記事でいう自動テストとは以下のようにテスト対象を実際に

masa8aurum 2020/05/28

初歩から詳しく書いてある

リンク

仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blog

こんにちは、SWETの鈴木穂高︵@hoddy3190︶です。私はこちらの記事に記載の通り、形式手法の可能性を模索しています。現在はツールやゲームの仕様を形式的に記述すること︵形式仕様記述︶で、仕様の欠陥をなるべく早く見つける取り組みにチャレンジしています。今回は仕様記述をするにあたりよく使う重要な記述テクニックである﹁Promotion﹂を紹介します。形式仕様記述とAlloyというツールを知っている人を対象にしています。もし形式仕様記述やAlloyをご存じない方は、以前私がbuilderscon tokyo 2019で発表したときに使った資料をご覧ください。 Promotionとは一般にソフトウェアシステムは複数のコンポーネントから構成されます。システム全体としての状態︵以下、システム状態︶は各コンポーネントの状態の組み合わせからなります。たとえどんなに奥深くのどんなに小さ

masa8aurum 2020/02/20

リンク

Coqで学ぶ証明プログラミング！テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！

Coqで学ぶ証明プログラミング！テストだけでなく﹁証明﹂で安全性を保証するプログラミング言語﹁Coq﹂では、プログラムを﹁証明﹂して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう！ coqtokyoを主催する今井宜洋さんの解説です。みなさん、Coqってご存知ですか？プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう！ Coqって何？プログラムを﹁証明する﹂ってどういうこと？ Coqを使ってみよう Coqのインストール方法 CoqIDE‥Coqによる証明開発のフロントエンド Coqで関数プログラミングプログラムの仕様を記述しよう証明開発モードゴ

masa8aurum 2019/01/18

証明プログラミング

リンク

はてなブックマーク

タグ

関連タグで絞り込む (3)

Formal-Methodに関するmasa8aurumのブックマーク (6)

お知らせ

今週のはてなブックマーク数ランキング（2024年7月第3週）

今週のはてなブックマーク数ランキング（2024年7月第2週）

はてなブックマーク透明性レポート（2024年 2月-2024年4月）

公式Twitter

キーボードショートカット一覧

はてなブックマーク

公式Twitter

はてなのサービス