Assertive Programming with SPARK (AdaCore GAP Workshop June 21, 2023)

Dr. Ran Ettinger, Ben-Gurion University of the Negev, Israel

This talk presents the adoption of SPARK alongside Dafny in an elective course given to third-year CS and SE students at Ben-Gurion University of the Negev. Being based on Rustan Leino's "Program Proofs" with example programs following Carroll Morgan's "Programming from Specifications", this course focuses on the detection of proof obligations for the formal verification of iterative and recursive code. This talk aims to show how SPARK and GNATprove are complementing the use of Dafny, demonstrating to students the industrial applicability of the learned approach. In this talk, as in the course, I show how manual annotation of a program with loop invariants, assertions, and ghost procedures for lemmas, with or without full proof, may justify the functional correctness of a developed program, both to the automated verifier and (as importantly) to the human reader. Adoption of open-source SPARK programs as a starting point for assignment exercises is discussed. Finally, one proof-authoring construct that I enjoy in Dafny is highlighted, hoping to inspire its addition to SPARK.

This talk was part of the 2023 GNAT Academic Program (GAP) Workshop. See the playlist for other talks. The GNAT Academic Program is an educational initiative that provides resources and support for academic institutions, enabling teachers and students to explore and utilize the Ada and SPARK programming languages. To learn more about GAP please visit our website at: https://www.adacore.com/academia