High Integrity Software: The Spark Approach to Safety and Security

Front Cover
Addison-Wesley, 2003 - Computers - 430 pages

This book provides an accessible introduction to the SPARK programming language.

  • Updated 'classic' that covers all of the new features of SPARK, including Object Oriented Programming.
  • The only book on the market that covers this important and robust programming language.
  • CD-ROM contains the main SPARK tools and additional manuals giving all the information needed to use SPARK in practice.
Technology:

The SPARK language is aimed at writing reliable software that combines simplicity and rigour within a practical framework. Because of this, many safety-critical, high integrity systems are developed using SPARK.

User Level:

Intermediate

Audience:

Software engineers, programmers, technical leaders, software managers. Engineering companies in fields such as avionics, railroads, medical instrumentation and automobiles. Academics giving MSc courses in Safety Critical Systems Engineering, System Safety Engineering, Software Engineering.

Author Biography:

John Barnes is a veteran of the computing industry. In 1977 he designed and implemented the RTL/2 programming language and was an original member of the ADA programming language design team. He was founder and MD of Alsys Ltd from 1985 to 1991. Currently self employed, John is the author of 'Programming in ADA' which has sold 150000 copies and been translated into 6 languages.

From inside the book

 

51 pages matching detail in this book

Where's the rest of this book?

Results 1-3 of 51

Contents

An Overview
1
Language Principles
23
SPARK Analysis Tools
53
Copyright

14 other sections not shown

Other editions - View all

High Integrity Software: The Spark Approach to Safety and Security : Sample ...
John Gilbert Presslie Barnes
No preview available - 2003

Common terms and phrases

abstract data type abstract own variable abstract state machine actual parameter array type assert assignment autopilot begin Chapter compiler components conditional statements constant corresponding data flow analysis declared defined derives annotation detail Do_It Door_History element(a end loop end record enumeration types Examiner example expression external variables File_Type Float Flow Error formal parameter full Ada global annotation global variables Go_Between identifier implementation important index file information flow analysis inherit clause initial value Inputs Integer range interface language main subprogram matrix mode Monitored_Stack Note object operations Outputs package body package specification path functions Pointer postcondition pragma precondition predefined private type procedure Proof Checker proof function record refinement renaming result return Integer return statement rules run-time checks Section Simplifier SPARK program Spark_IO static subtype subtype_mark subunit syntax The_Stack The_Stack.State true type Integer type Stack updated Use_Stack verification conditions visible write

References to this book

Bibliographic information

TitleHigh Integrity Software: The Spark Approach to Safety and Security
AuthorJohn Gilbert Presslie Barnes
Editionillustrated, reprint
PublisherAddison-Wesley, 2003
Original fromthe University of Michigan
DigitizedNov 17, 2007
ISBN0321136160, 9780321136169
Length430 pages
Subjects ›  › 

Computers / Languages / General
Computers / Programming / General
Computers / Programming Languages / Ada
Computers / Security / General
Computers / Software Development & Engineering / General
  
Export CitationBiBTeX EndNote RefMan