CS 633G - Ada Programming Using the SPARK Approach

This course explores the SPARK restricted Ada-subset, annotated meta-information in SPARK as Ada comments, component behavior and runtime requirements, design-by-contract principles, formalization and validation of runtime behavior.

Prerequisite: CS 631G - Ada Real-Time Programming or equivalent.
Credits: 3
NOTE:
* This course is taught by the Institute for Academic Outreach.