Building High Integrity Applications with SPARK

Building High Integrity Applications with SPARK

McCormick, John W. (University of Northern Iowa); Chapin, Peter C.

Cambridge University Press






15 a 20 dias

The formally defined programming language SPARK provides a means to guarantee that a computer program has no errors. This makes it a natural system for designing safety- and security-critical applications. This first introduction to SPARK 2014 will allow students and developers to master the basic concepts for building systems with SPARK.
1. Introduction and overview; 2. The basic SPARK language; 3. Programming in the large; 4. Dependency contracts; 5. Mathematical background; 6. Proof; 7. Interfacing with SPARK; 8. Software engineering with SPARK; 9. Advanced techniques.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.