株式会社極東書店トップ > 商品一覧 > Building High Integrity Applications with SPARK.
商品詳細
Building High Integrity Applications with SPARK.
・ISBN 978-1-107-65684-0 paper GB£ 51.00
¥16,156.- (税込) ※(※)価格はご注文時の参考価格となります。
納品価格につきましては書籍の入荷時点で確定となります。
版元の原価改定、外国為替の変動等により異なる場合がございますので、予めご了承下さい。
お気に入り
★★★
| 著者・編者 | McCormick, John W. / Chapin, Peter C., |
|---|---|
| 出版社 | (Cambridge University Press, UK) |
| 出版年月 | 2015 |
| ページ数 | 382 pp. |
| 言語 | ENG |
| ニュース番号 | <A00-6170> |
解説
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.