Home | Contact | Pricing | News | Events | Partners | Mailing List | Site Map

Gnat Pro – Professional Training

Master Ada and GNAT Pro

Get training from some of the foremost experts on the Ada programming language and GNAT Pro technology. Experience has shown that Ada is an extremely learnable language and that programmers with basic knowledge in other languages can quickly get up to speed with Ada. For programmers who already have some Ada experience, AdaCore offers advanced courses in Ada and GNAT Pro/GPS designed to help developers get the most out of the technology.

Training sessions can be given on-site or at AdaCore’s New York City headquarters. For information regarding scheduling, pricing or custom training sessions, please contact sales@adacore.com


Programming Courses

  • Ada Fundamentals

    5 Day
    Course Description
    This course provides a full introduction to programming in Ada. Classic programming features are discussed, with an emphasis on Ada’s support for constructing modular, portable, and reliable systems. Depending on the subjects of interest, this course could be specific to any version of the language, Ada 95, Ada 2005 and Ada 2012.
    Target Audience
    Programmers interested in learning the fundamentals of Ada software development.
    Course Duration
    5 Day Customizable Course
    Course Contents

    The core content of the course include the following topics:

    • Fundamental data types: integer (including modular) types, enumeration types, real types, record and array types
    • Basic algorithmic features (expressions, statements, subprograms)
    • Limited types
    • Exceptions and exception handling
    • Modular program construction using packages, private types, and child library units
    • Overview of access types
    • Overview of generic units

    In addition to the core contents of the course, an overview on one of the following subject can be selected:

    • Object-oriented programming
    • Low-level programming
    • Concurrent programming
    If you are interested in another overview topic, please contact us on sales@adacore.com.
  • Ada Advanced Topics

    5 Day
    Course Description
    Advanced Ada users can improve their skill by learning advanced Ada programming techniques. Such course will be given in 5 days, and the contents can be picked up from the items below. Longer courses are possible if needed. Depending on the subjects of interest, this course could be specific to any version of the language, Ada 83, Ada 95, Ada 2005 and Ada 2012.
    Target Audience
    Programmers interested in learning advanced Ada software development topics. Programmers should be familiar with the content of the course “Ada Fundamentals”.
    Course Duration
    5 Day Customizable Course
    Course Contents

    The core content of the course include the following topics:

    • Access types
    • Generic units
    • Predefined library
    • Runtime and user-defined checks

    In addition to the core contents of the course, a special emphasis can be given to one or two of the following subjects:

    • Concurrent programming
    • Object-oriented programming
    • Low-level programming
    • Programming in the large
    • Specialized Needs annexes overview
    If you are interested in another overview topic, please contact us on sales@adacore.com.
  • Multi-language programming

    1-4 Days
    Course Description
    This course is targeted to Ada developers wishing to build mixed language application, using Ada an an other language. Manual and automatic interfacing mechanisms will be described, as well as build procedures and debug environments.
    Target Audience
    Programmer familiar with Ada basics and the language they’re intending to mix Ada with.
    Course Duration
    1-4 days
    Ada and C – 1 day
    • Manually interfacing C and Ada code through pragma Interface
    • Automatic code binding generation
    • Advanced Ada and C type mapping
    • Integrated build through gprbuild
    Ada and C++ – 1 day
    • Manual interfacing of C++ and Ada code through pragma Interface
    • Automatic code binding generation
    • Cross language inheritance and dispatching between Ada tagged types and C++ classes
    • Integrated build through gprbuild
    Ada and Java – 1 day
    • Manual interfacing of C++ and Java code through JNI
    • Automatic binding generation through GNAT-AJIS
    • Cross language inheritance and dispatching between Ada tagged types and Java classes
    • Mixed Ada / Java application build
    • Mixed Ada / Java application debugging
    Ada and Python – 1 day
    • Manual interfacing of Ada and Python Code through GNATColl
    • Calls python script & code from Ada
    • Export Ada code and types to Python
  • Hard Real-Time and Embedded Systems Programming

    4 Days
    Course Description
    Although the terms are often used interchangeably, real-time systems need not be embedded, and embedded systems need not have deadlines. However, applications in both domains are expensive and labor-intensive, especially because developers typically have only low-level tools available and must use techniques that are more ad hoc than analytical. Ada 2005 represents the state-of-the-art in real-time programming languages and offers a high-level model for low-level programming that is unsurpassed in expressive power. This intensive course covers the modern analytical techniques for determining whether deadlines will be met, the Ada language facilities required to support those analyses, and the high-level model Ada provides for embedded systems development. In addition, the issues involved in storage management are covered so that, in addition to time, equally important storage resources are available when required.
    Target Audience
    Developers interested in learning or perfecting their real-time and embedded programming skills with this state-of-the-art language. This course is intended for developers familiar with some of the more advanced features of Ada, including tasking and access types.
    Course Duration
    4 days
    Course Contents
    • Low-Level Programming
    • Schedulability Analysis
    • Schedulability Analysis Support in Ada
    • Language-defined Tasking Facilities
    • Reliable Storage Management
    • Performance Issues

SPARK Courses

  • Software Engineering with SPARK

    4 Day
    Course Description
    A 4-day course for managers, regulators and engineers, which presents the principles of the development of high assurance software, and the related certification requirements. It then explains the rationale of SPARK, outlines the language and the principles of static code analysis, and presents the role of the SPARK Toolsuite in systematic program development. The course also covers fundamental SPARK design issues, such as appropriate use of packages such as abstract machines and data types, as well as the use of SPARK refinement, system interfaces, library mechanisms, etc. Some of the more advanced facilities of the SPARK Examiner, for run-time error checking for example, are presented.

    This course includes extensive hands-on sessions using the SPARK Pro Toolsuite.
    Target Audience
    Software Engineers, Managers and Evaluators who need a full understanding of SPARK and its capabilities.
    Course Duration
    4 Day Course
    Course Contents
    • Rationale of SPARK
    • Design building blocks – ADTs anD ASMs
    • The SPARK language – types, expressions, statements,subprograms, packages
    • Information-flow analysis
    • Setting up a SPARK project
    • INFORMED Design approach for SPARK
    • Abstraction and State Refinement
    • Interfacing to other languages
    • Introduction to proof
  • Advanced SPARK course

    1-5 Day
    Course Description
    This course covers advanced SPARK topics – it can be composed of a combination of several topics described below.
    Target Audience
    Experienced SPARK users who with to learn how to exploit the SPARK proof system and advanced tools.
    Course Duration
    1-5 Day Customizable Course
    Advanced SPARK Program Design and Verification – 3 day
    This course covers the advanced use of SPARK, particularly in the context of proof of exception freedom and code correctness. Attendees are taught to understand the relationship between SPARK source code and the verification conditions generated for proof, leading to an understanding of the impact of good SPARK design principles on code verification. Advanced facilities of the SPARK Examiner are presented, and tuition in planning, conducting and managing the verification activities is supplemented by the use of the SPARK proof tools, particularly the Simplifier.

    The course has a strongly practical flavour, interweaving guidance and lecture material with topical tutorial sessions which reinforce the lecture material via relevant examples. Each tutorial session commences with a step-by-step example which provides detailed guidance, followed by additional exercises which can be tried in the tutorial sessions or used after the course to gain additional practical experience.

    This course includes extensive hands-on sessions using the SPARK Pro Toolsuite. Note that this course does not cover the RavenSPARK language profile or the use of the Proof Checker tool.
    • Designing with proof in mind
    • The FDL proof language and logic
    • Representation of SPARK in FDL
    • Understanding VCs
    • Arrays, Quantifiers and Loops
    • Management of Proof Complexity
    • The Proof Cycle
    • Validation of input data
    • Real numbers, private types, and refinement
    Concurrent Software Design with RavenSPARK – 1 day
    The Ada95 Ravenscar profile defines a subset of the Ada95 tasking facilities that are appropriate for the construction of high assurance software. This one-day course introduces the Ravenscar profile and how it has been included in the core SPARK language. The course covers the additional contracts in SPARK that are used to describe packages that contain tasks and protected objects and the additional analyses implemented by the Examiner to eliminate the potential for defects in Ravenscar programs.
    • Ravenscar profile basics
    • Tasks
    • Protected state
    • Atomic variables and suspension objects
    • Interrupts
    • Inter-task information-flow analysis
    • Proof and run-time errors in RavenSPARK
    Introduction to the Proof Checker – 1 day
    This course introduces the SPARK Proof Checker, and how it can augment the abilities of the Examiner and Simplifier in the verification of SPARK programs. Attendees will cover the basics of using the Checker’s interactive proof engine to prove VCs that remain after simplification. The course also covers the use of the Proof Checker to establish the validity of user-defined proof rules.
    • Introducing the Proof Checker
    • Basic proof strategies – inference and substitution
    • Proof patterns and commands – proof by cases, contradiction, deduction and standardization
    • Proof rules – validity and properties
    • Proof management – maintenance of rules and proof scripts
  • SPARK – Overview

    2 day
    Course Description
    A 2-day “extended tutorial” for managers and engineers that presents the principles and practice of high assurance software engineering with SPARK.

    The course explains the rationale of SPARK, outlines the language and the principles of static code analysis, and presents the role of the SPARK Pro Toolset in systematic program development. The course also covers the design of the SPARK language and the various types of analysis and verification that can be performed. The second day of the course concentrates on practical issues, such as how SPARK matches contemporary standards for high assurance software and software processes such as CMM and PSP/TSP. Finally, the issues (and problems) of adopting SPARK will be considered, followed by case-studies of SPARK usage in the aerospace, rail and security domains.

    This course includes some pencil-and-paper exercises, but does not involve computer-based practical sessions, SPARK programming or extensive use of the SPARK Pro toolsuite. Students requiring a thorough understanding of the practical use of the SPARK Pro Toolsuite are referred to the longer “Software Engineering with SPARK” course.
    Target Audience
    Software Engineers, Managers and Evaluators who need a full understanding of SPARK and its capabilities.
    Course Duration
    2 Day Course
    Course Contents
    • Rationale of SPARK
    • Design building blocks – ADTs anD ASMs
    • The SPARK language – types, expressions, statements,subprograms, packages
    • Verification
      • Subset and static semantics
      • Information flow analysis
      • Formal verification
      • Security topics
    • SPARK and Standards
    • SPARK and Software Process
    • ROI and Adoption
    • SPARK Projects
  • Refresh your SPARK

    1 Day *
    Course Description
    A one-day “refresher” course for engineers that have used SPARK in the past, using earlier versions of the language and toolset. It is assumed that students will have used the SPARK Examiner in the past, but not the Simplifier or other proof tools.

    The course covers a reminder of the basics of SPARK: the language subset, use of the Examiner, information-flow analysis and the diagnosis and correction of common design errors. The course goes on to cover more recent development, such as the SPARK95, SPARK2005 and RavenSPARK language profiles, the INFORMED design style for SPARK, the basic use of the proof tools to establish the absence of runtime errors, and the impact of SPARK on other areas of the software process, such as reviewing and testing.

    The course will also cover the new SPARK Pro package with the GPS IDE, case studies and an overview of new language and toolset features. This final section can be customized to suit the students’ particular most-recent experience with SPARK.

    The course does not involve hands-on use of the SPARK tools, but there are several “pencil and paper” exercises and demonstrations of the toolset in action.
    Target Audience
    Engineers that have used SPARK previously, but need to be brought up to date with the latest developments in the SPARK language and toolset.
    Course Duration
    1 Day Course
    Course Contents
    • SPARK basics reminder – subset and contracts
    • Information and Data-Flow Analysis
    • Common Errors and their Diagnosis
    • INFORMED Design in SPARK
    • Runtime Error Proof – Just Try It!
    • Adjusting the Software Process for SPARK
    • Case Studies – Tokeneer and others
    • SPARK Pro and GPS
    • What’s new in SPARK since version X?
    • Future development Roadmap

AdaCore Tools and Technology Courses

  • Static Analysis tools

    1 Day *
    Course Description
    This course shows how to use advanced static analysis tools to improve overall code quality and enforce programming styles. It also will show how to take advantage of the GNAT compiler options in order to spot obvious programmer errors early in the development process, and how to take advantage of stack usage data that can be extracted at compile-time.
    Target Audience
    Developers interested in learning how to deploy and use static analysis tools to improve code quality and safety, as well as quality engineers or people responsible for software safety.
    Course Duration
    1 day
    Course Contents
    • Advanced usage of compiler check and warnings
    • GNATcheck – automatic style check verification
    • GNATelim – dead code elimination
    • GNATstack – static stack usage analysis
  • Dynamic Analysis tools

    1 Day *
    Course Description
    This course shows how to use advanced dynamic analysis tools to improve overall testing and debugging operation when using the GNAT Pro toolset. It will in particular covers topics such as code coverage, unit testing and profiling. In addition, specific compiler switches and pragma allowing to detect additional errors will be studied.
    Target Audience
    Developers interested in learning how to deploy and use testing and dynamic analysis tools, as well as quality engineers or people responsible for software safety.
    Course Duration
    1 day
    Course Contents
    • Compiler switches and pragmas
    • Advanced usage of the debugger
    • AUnit – unit testing
    • GCOV – native coverage analysis
  • CodePeer

    1 Day *
    Course Description
    This course shows how to use CodePeer to statically detect and analyses potential run-time and logic errors. Emphasis will be given on how to integrate such a technology in a development process and how to take advantage of its capabilities on a day by day basis.
    Target Audience
    Developers interested in learning how to deploy and use static analysis tools to improve code quality and safety, as well as quality engineers or people responsible for software safety.
    Course Duration
    1 day
    Course Contents
    • Runtime errors detection
    • Logic errors detection
    • Automated code review
    • Test vectors and test cases generation
  • GNAT Pro with GPS

    3 Days
    Course Description
    This course shows advanced usage of GPS, and how to improve productivity by using its most advanced features. It’s composed of three independent days which can either be taken as a part of a GPS course, or separated and combined with other topics.
    Target Audience
    Developers interested in learning how to use GNAT Pro and GPS.
    Course Duration
    3 days, including (and possibly mixed with others)
    Advanced GPS usage for edition and debug – 1 day
    • Edition features
    • Advanced navigation
    • Documentation generation
    • Code completion
    • Integrated Debugger
    • Integrated builder
    • Remote programming
    GNAT toolchain and Project Management – 1 day
    • Understanding the GNAT toolchain
    • GNAT options and pragmas
    • Advanced setup of GNAT Project files
    • Scenario configuration
    • Usage of gnatmake and gprbuild
    GPS customization – 1 day
    • Python basics
    • Existing GPS plugin
    • Extending GPS via XML
    • Extending GPS via Python
    • Driving GPS from the command line
  • GNAT Pro with GNATbench

    2 Days
    Course Description
    This course will thoroughly cover GNATbench, the AdaCore Eclipse plug-in for GNAT Pro Ada used to develop applications with Eclipse. Students will become thoroughly familiar with the use of GNATbench for building native or cross applications. This course can be customized either for standard Eclipse, or WindRiver Workbench.
    Target Audience
    Developers interested in learning how to use GNAT Pro and GNATbench.
    Course Duration
    2 days
    Advanced GNATbench usage for edition and debug – 1 day
    • The standard Eclipse graphical user interface
    • Edition features
    • Advanced navigation
    • Code completion
    • Integrated Debugger
    • Integrated builder
    GNAT toolchain and Project Management – 1 day
    • Understanding the GNAT toolchain
    • GNAT options and pragmas
    • Advanced setup of GNAT Project files
    • Scenario configuration
    • Usage of gnatmake and gprbuild
  • GtkAda

    3 Days
    Course Description
    After the first day, students will have acquired a good knowledge of the building blocks and general principles of GtkAda, and will have built their first GtkAda application. The second day covers advanced features of the toolkit, along with “best practice” principles. At the end of this day, students will have enough knowledge to write and maintain GtkAda applications. The third day provides an advanced look at the most complex widgets of GtkAda, which are often the heart of GtkAda applications.
    Target Audience
    Ada programmers interested in learning graphical user interface (GUI) development
    Course Duration
    3 days
    Course Contents
    • Introduction to GtkAda
    • Building blocks of GtkAda: Glib, Gdk, Gtk, Pango, Cairo
    • Configuring and installing GtkAda
    • Structure of a GtkAda application
    • Graphical layout: the Widgets hierarchy
    • The Gtk main loop: signals and events
    • Using the Glade-3 GUI builder
    • Layout of the widgets
    • Creating your own widgets
    • GtkAda and tasking
    • Good development practices with GtkAda
    • Advanced uses of the main loop: Idle and Timeout callbacks
    • GtkAda Widgets: Canvas and MDI
    • Low-level drawing with Cairo
    • Using the Tree_View
    • Using the Text_View

Contact Us

For further information or registration forms, or to arrange for any of these courses to be delivered on site at your facility, please contact sales@adacore.com

* A minimum of 3 days of training is required for on-site visits.