このチュートリアルは、SVGファイルとしてアニメーションロゼッタ（ハイポトロコイド）を生成するプログラムを作成することで、Adaの機能を示しています。Ada 2022の機能を使用し、AdaのパッケージマネージャーであるAlireを活用してプロジェクトを管理します。このチュートリアルでは、Adaの可読性、強い型付け、安全性に焦点を当て、幾何学的計算とSVGレンダリングにおけるAdaの使用方法を示します。著者は、Adaが安全性が重要なアプリケーションで知られているにもかかわらず、現代的な汎用言語として適していることを強調しています。
続きを読む
増え続けるサイバーセキュリティの脅威に対処するため、NVIDIAのセキュリティチームは従来のテスト手法を放棄し、SPARKによる形式的検証を採用しました。わずか3ヶ月で、セキュリティに重要なCコードをSPARKに変換することに成功し、パフォーマンスを低下させることなくセキュリティを向上できることを実証しました。現在、50名以上のNVIDIA開発者がSPARKのトレーニングを受けており、多くの製品にSPARKコンポーネントが搭載されています。この事例研究は、形式的検証の成功事例であり、セキュリティ強化を目指す他の組織にとって貴重な教訓となります。
続きを読む
2024年度Ada/SPARK Crate of the Year Awardsの結果が発表されました！Lionel Draghi氏が、自動テストのために分かりやすいMarkdown形式の動作仕様書を使用するコマンドラインツールBBTでAda Crate of the Yearを受賞しました。Kevin Chadwick氏は、メモリセーフなログライブラリelogs（SPARKシルバー認定）でSPARK Crate of the Yearを受賞しました。このライブラリは、ユーザーが最大メッセージ長を指定できます。最後に、Brent Seidel氏の組み込み可能なLispインタプリタbbs_lispがEmbedded Crate of the Yearを受賞し、組み込みシステムにおけるAdaの強みを示しました。
続きを読む