相關主題
商品描述
Software is pervasive in our lives. We are accustomed to dealing with the failures of much of that software - restarting an application is a very familiar solution. Such solutions are unacceptable when the software controls our cars, airplanes and medical devices or manages our private information. These applications must run without error. SPARK provides a means, based on mathematical proof, to guarantee that a program has no errors. SPARK is a formally defined programming language and a set of verification tools specifically designed to support the development of software used in high integrity applications. Using SPARK, developers can formally verify properties of their code such as information flow, freedom from runtime errors, functional correctness, security properties and safety properties. Written by two SPARK experts, this is the first introduction to the just-released 2014 version. It will help students and developers alike master the basic concepts for building systems with SPARK.
商品描述(中文翻譯)
軟體在我們的生活中無處不在。我們已經習慣於處理許多軟體的故障——重新啟動應用程式是一個非常熟悉的解決方案。然而，當軟體控制我們的汽車、飛機和醫療設備，或管理我們的私人資訊時，這些解決方案是不可接受的。這些應用程式必須無錯誤地運行。SPARK 提供了一種基於數學證明的方法，以保證程式沒有錯誤。SPARK 是一種正式定義的程式語言和一組驗證工具，專門設計用於支持高完整性應用程式的軟體開發。使用 SPARK，開發人員可以正式驗證其程式碼的屬性，例如資訊流、無執行時錯誤、功能正確性、安全性屬性和安全性屬性。這本書由兩位 SPARK 專家撰寫，是剛剛發布的 2014 版本的首次介紹。它將幫助學生和開發人員掌握使用 SPARK 建立系統的基本概念。
