Logic for Programmers by Hillel Wayne

Logic for Programmers 数学、ソフトウェア、そしてそれらを使って後者を改善することについての本。実務のプログラマーのために書かれています。数学の予備知識は不要です。印刷版を購入する電子書籍を購入する電子書籍サンプル章サンプル227ページ。電子書籍にはDRMフリーのPDFとEPUBが含まれます。この本は何ですか？これは、ソフトウェアの設計、検証、推論をより良くするための本です。そして、論理学、つまりブール代数を少し学ぶことで、私たちの分野のあらゆるクールなテクニックがアンロックされることについても書かれています。どのようなものか感じをつかみたい場合は、サンプル章を読んでみてください！これは主に理論的なものですか、それとも実用的な応用もありますか？本の中のすべては実用的であることを意図しています。初期の章は、「条件分岐の単純化」や「APIの変更がクライアントを壊さないことを保証する」といったトピックについてです。後期の章は、「仮想的なソフトウェア設計における競合状態の発見」や「分散タスクの壁時計時間の最小化」といった、少し難解なテーマについてです。すべてがすべての人に役立つわけではありませんが、誰もが何か役立つものを見つけてくれることを願っています！数学の知識は必要ですか？いいえ！プログラマーが日常的に経験を通じて習得するブール代数のAND、OR、NOT以外に数学の知識は必要ありません。本はあなたが必要とする残りの数学をカバーしています。とはいえ、プログラミングの知識は必要です！この本は中級から上級のプログラマーを対象としており、ループ、バージョン管理、テストなどの普遍的なトピックを読者が知っていると仮定しています。一部の章では、SQLやAPI設計のようなより具体的な知識が期待されます。ただし、章は独立しているので、ニーズに合わないものがあれば、遠慮なくスキップしてください。タイトルにある奇妙なAとEは何ですか？論理学者はそれぞれ「すべて」と「存在する」を意味する記号∀と∃を使用します。例えば、「すべての人は好きな色を持っている」という文は、∀p ∈ Person: ∃c ∈ Color: IsFavoriteColor(p, c)と書くことができます。トピックの学習（および本の検索）を容易にするために、数式記号の代わりに英単語を使用しています。したがって、同じ式は、すべてのp ∈ People: (some c ∈ Color: IsFavoriteColor(p, c))となります。どうすれば入手できますか？スマートフォンやコンピューターで本を読みたい場合は、PDFまたはEPUBとして入手できます。こちらがPDFです：印刷版は、白黒印刷とより広いページ余白を除いて同じです。Amazonで購入できます。本には何が含まれていますか？以下は目次と対応するテクニックです：論理学の速習コース • 述語、ブール値、集合、量化子コードのリファクタリング • 書き換えルールより良いテストを書く • プロパティテストコードの合成 • 契約、サブタイピングコードの証明 • 形式検証、Dafnyデータとの作業 • データベース理論意思決定の解読 • 決定表ドメインのモデリング • 形式仕様、Alloyシステムの設計 • 時相論理、TLA+数学の問題を解く • 制約およびSMTソルバー論理プログラミング • PrologおよびAnswer Set Programmingさらに、数学表記、便利な書き換えルール、論理学の高度なトピックに関するいくつかの付録があります。すべてのコードサンプルはGitHubで入手できます。また、本には使用されていない同じトピックに関する追加のサンプルも多数あります。本はどのくらいの長さですか？約50,000語、200ページ強です。追加クレジットはさらに約4,000語です。「追加クレジット」とは？カバーしたかったが、本に含めるには有用性や焦点が絞られていなかった興味深いトピックがたくさんあります。そのため、それらを「追加クレジット」リポジトリに入れ、本にリンクを貼りました。これには、状態空間のサイズの計算方法、半順序理論、その他のいくつかの小さなトピックが含まれます。Pythonではなぜ all([]) == True なのですか？それはいつも私を悩ませていました。Pythonのall関数は次と同等です：all(l) = l[0] && l[1] && l[2] ...これには特定の性質があります：任意の2つのリストxsとysに対して、次のことがわかります：all(xs . ys) == all(xs) && all(ys)しかし、これは任意の2つのリストについてであり、空のリストも含まれます！ys = []を選んだらどうなりますか？すると、xs . [] == xsとなり、次のようになります：all(xs) && all([]) == all(xs . []) all(xs) && all([]) == all(xs)もしall([]) = Trueなら、この方程式はall(xs) && True == all(xs)、つまりall(xs) == all(xs)となります。もしall([]) = Falseなら、これはall(xs) && False == all(xs)となり、これはxsが何であってもall(xs) == Falseを意味します。したがって、この性質を維持するためにはall(xs) = Trueである方が理にかなっています。Trueは&&の恒等元であると言います：p && True == p、pが何であっても。ちなみに、同じ議論は、空リストの合計が0であり、空リストのanyがFalseである理由も説明しています。著者は誰ですか？私は形式手法、分散システム、ソフトウェア史を専門とするソフトウェアエンジニアです。過去の作品には、Practical TLA+やThe Crossover Projectがあります。NASA、Meta、Giesecke+Devrient、McKinsey & Company、Siemens AG、Western Digitalなどのクライアントのために形式検証とトレーニングを行ってきました。カンファレンスで話すときは、いつも自家製チョコレートを持っていきます。ブログと週刊ニュースレターも発行しています。読む準備はできましたか？印刷版を購入する電子書籍を購入するサンプル