Articles Tagged “SPARK”
5 articles tagged “SPARK”, newest first.
-
Starting an Ada Project with Alire — Creating a Project, Adding Dependencies, Build Profiles, and GNATprove
Using Alire, the Ada package manager, to create a project, fetch GNAT automatically, add crates, switch build profiles, and prove code with GNATprove, with r...
-
How Ada and Rust Think About Safety — Comparing Types, Overflow, Ownership, Data Races, and Formal Verification by Running Them
Ada and Rust both put safety first, but they stop errors in different places. We compare value ranges, overflow, memory, data races, unchecked escapes, and f...
-
Proving AI-Written Code with SPARK ── Humans Write the Contracts, GNATprove Checks Them
We add preconditions and postconditions to Ada functions written by AI and prove them with GNATprove, using real output: how to read failures, proofs that pa...
-
Introduction to Formal Verification with SPARK — From Ada Contracts to Mathematical Proof
A practical introduction to formal verification using the SPARK subset of Ada. Covers how to step up from contracts (Pre/Post) to proofs, using GNATprove, lo...
-
The Appeal of the Ada Language — Expressing Design Through Types and Powering Software That Runs for Decades
An introduction to the appeal of the Ada language: strong typing, range constraints, separation of specification and implementation via packages, design by c...