Spark Ada

Question 1

What is Ada the required standard for?

Answer 1

Military applications in the US. Ada was first designed for these military applications.

Question 2

What does Ada have instead of methods?

Answer 2

Functions and procedures

Question 3

Is Ada case senstitive?

Answer 3

No

Question 4

What is a package?

Answer 4

A collection of types, global variables, functions and procedures.

Question 5

Why is Ada used in critical systems?

Answer 5

Ada was specifically designed for real time critical systems more specifically military applications.

Question 6

What is SPARK Ada?

Answer 6

A formally verified subset of Ada, aiming to enhance software reliability, safety, and security in critical systems by leveraging formal methods and static analysis tools to mathematically prove properties about the software’s behaviour.

Question 7

How many levels of analysis does SPARK Ada have?

Answer 7

3 Levels

Question 8

What is analysed in Level 1 analysis of Spark Ada?

Answer 8

The correct Ada syntax is used.

Question 9

What is analysed in Level 2 of Spark Ada?

Answer 9

Data flow analysis and Information flow analysis.

Question 10

What is data flow analysis?

Answer 10

• Checks input/output behaviour of parameters and variables
• Checks initialisation of variables
• Checks that changed and imported variables are used later

Question 11

What is information flow analysis?

Answer 11

Verifies interdependencies (multiple dependencies) between variables

Question 12

What is analysed in Level 3 of SPARK Ada?

Answer 12

• Generation of verification conditions
• Proof of verification conditions

Question 13

What does SPARK Ada restrict?

Answer 13

• Function side effects
• Control on the amount of memory used

Question 14

What must be added to a program file to active SPARK Mode?

Answer 14

pragma SPARK_MODE(On)

Question 15

What is Pragma?

Answer 15

Annotations to a unit in Ada

Question 16

What are aspects?

Answer 16

Annotations to a package, procedure or function.

Question 17

How does SPARK Ada address logical soundness?

Answer 17

Functions can have side effects, but if the order of evaluation matters, functions with side effects are not allowed

Question 18

How does SPARK Ada address simplicity of language definitions?

Answer 18

It omits too complex principles such as:
- No variant records
- No threads
- No generic types.

Question 19

How does SPARK Ada address the Expressive Power criteron?

Answer 19

• Allows hiding of variables
• Allows you to specify strong assertions about variables. E.g. in and out variables

Question 20

How does SPARK Ada address the Security criteron?

Answer 20

In order to be verifiable at compile time constraints have to be static

Question 21

How does SPARK Ada address the verifiability criteron?

Answer 21

Supports automated verifiability with extra annotations:
- control of data flow
- control of information flow
- proof annotations

Question 22

Why does Spark Ada not allow side effects?

Answer 22

To ensure that the system has predictable behaviour. Side effects can lead to unpredictable changes which is a threat to safety.