SPARK (programming language) facts for kids
 |
|
| Paradigm | Multi-paradigm |
|---|---|
| Developer | Altran and AdaCore |
| Stable release |
Community 2021 / June 1, 2021
|
| Typing discipline | static, strong, safe, nominative |
| OS | Cross-platform: Linux, Microsoft Windows, Mac OS X |
| License | GPLv3 |
| Website | About SPARK |
| Major implementations | |
| SPARK Pro, SPARK GPL Edition, SPARK Community | |
| Influenced by | |
| Ada, Eiffel | |
SPARK is a special computer programming language. It is based on the Ada language. SPARK is used to create very reliable software. This software is for systems where things must work perfectly. It helps build apps that need to be super safe and secure.
There have been different versions of SPARK. The first ones were SPARK83, SPARK95, and SPARK2005. These were based on older versions of Ada. A newer version, SPARK 2014, came out in 2014. It was a big update to the language and its tools.
SPARK uses a specific part of the Ada language. It adds "contracts" to describe how parts of a program should work. These contracts help check the code for mistakes. In older SPARK versions, contracts were hidden in comments. But in SPARK 2014, they are a main part of the language. This makes it easier for tools to understand them.
Contents
What Makes SPARK Special?
SPARK uses the good parts of Ada. It tries to remove any confusing or unsafe features. SPARK programs are designed to be clear. They should always work the same way, no matter which Ada compiler is used. This is done by leaving out some tricky Ada features. It also uses contracts to explain what a program is supposed to do.
These ideas help SPARK meet its main goals:
- It is logically correct.
- It has clear rules.
- It is simple to understand.
- It is very secure.
- It can express complex ideas.
- It is easy to check for errors.
- It uses computer resources efficiently.
- It needs very little extra software to run.
How Do SPARK Contracts Work?
Contracts are like rules for your code. They tell you what a piece of code should do. Let's look at an example. Imagine a simple command called `Increment`.
procedure Increment (X : in out Counter_Type);
In regular Ada, this command could do many things. It might add one to `X`. It could also add a thousand. It might even do nothing at all with `X`. This makes it hard to know what will happen.
Adding Rules with Contracts
With SPARK 2014, you add contracts to explain the code. For example, you could say:
procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X);
This contract tells us two things. First, the `Increment` command does not use any "global" variables. Global variables are ones that can be changed from anywhere in the program. Second, it says that the new value of `X` only depends on its old value. This makes the code's behavior very clear.
You can also add more detailed rules:
procedure Increment (X : in out Counter_Type) with Global => (In_Out => Count), Depends => (Count => (Count, X), X => null);
This contract explains that `Increment` uses a global variable called `Count`. It also says how `Count` and `X` change. The tools that check SPARK code compare these rules to what the code actually does. If there's a difference, it tells the programmer.
Setting Conditions for Code
Contracts can also set conditions for when a command is called. These are called preconditions. They can also set conditions for what will be true after a command runs. These are called postconditions.
For example:
procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X), Pre => X < Counter_Type'Last, Post => X = X'Old + 1;
This contract says a few things. It still says `X` only depends on itself. But it also adds:
- Pre-condition: Before `Increment` runs, `X` must be less than its largest possible value. This stops the number from getting too big.
- Post-condition: After `Increment` runs, `X` will be exactly one more than its original value.
Checking for Errors with SPARK
SPARK tools can also create "verification conditions." These are like math problems. They help prove that certain things are true about your program. The tools check for common errors, such as:
- Trying to access an array outside its limits.
- Numbers going beyond their allowed range.
- Dividing by zero.
- Numbers getting too big (overflow).
If you add post-conditions or other rules, the tools also check them. They make sure these rules hold true for every possible way the program can run. The SPARK tools use other special programs to solve these math problems.
A Brief History of SPARK
The first SPARK language was created at the University of Southampton. This was in the UK. Its name, SPARK, came from SPADE Ada Kernel. It was like a special part of the Ada language.
Over time, SPARK was improved and expanded. Different companies worked on it. In 2009, a company called Praxis teamed up with AdaCore. They released "SPARK Pro" and a free version for students. In 2010, SPARK was chosen for a US Lunar project called CubeSat. The newest version, SPARK 2014, was released in 2014.
Where is SPARK Used?
SPARK is used in places where software must be extremely reliable.
Making Systems Safe
SPARK has been used in many important safety systems. These include:
- Airplanes: Parts of jet engines and flight systems.
- Military Aircraft: Software for fighter jets.
- Air Traffic Control: Systems that manage airplanes in the sky.
- Trains: Many railway signaling applications.
- Medical Devices: Like heart-assist devices.
- Space: Projects like the Vermont Technical College CubeSat project.
Keeping Systems Secure
SPARK is also used to build secure systems. For example:
- Secure Solutions: For companies like Rockwell Collins.
- Government Security: Used in projects for the NSA.
- Firmware: NVIDIA uses SPARK for secure firmware.
In 2010, an engineer used SPARK to create a part of a new security system. It was almost as fast as code written in the C language. Later, it became just as fast. In 2020, another engineer rewrote a cryptography library in SPARK. The SPARK version was proven to be very safe and even faster.
See also
- Z notation
- Java Modeling Language
