# Test and Proof¶

## Various Combinations of Tests and Proofs¶

Overall context is functional verification of code

Combination can take various forms:

- Test before Proof – contracts used first in test, possibly later in proof
- Test for Proof – contracts executed in test to help with development of proof
- Test alongside Proof – some modules are tested and other modules are proved
- Test as Proof – exhaustive test as good as proof
- Test on top of Proof – proof at unit level completed with test at integration level, also using contracts

## Test (be)for(e) Proof¶

### Activating Run-time Checks¶

Need to activate run-time checks in executable

`Constraint_Error`

exceptions activated by default- Use
`-gnat-p`

to revert effect of previous`-gnatp`

(say in project file) - Use
`-gnato`

to activate overflow checking (default since GNAT 7.3)

- Use
Special handling of floating-point computations

- Use
`-gnateF`

to activate bound checking on standard float types - Use
`-msse2 -mfpmath=sse`

to forbid use of 80bits registers and FMA on x86 processors - Runtime/BSP should enforce use of Round-Nearest-tie-to-Even (RNE) rounding mode

- Use

### Activating Assertions¶

Need to activate assertions in executable

`Assertion_Error`

exceptions deactivated by default- Use
`-gnata`

to activate globally - Use pragma
`Assertion_Policy`

to activate file-by-file - Use
`-gnateE`

to get more precise error messages (`Contract_Cases`

)

- Use
Special assertions checked at run time

`Contract_Cases`

⟶ checks one and only one case activated`Loop_Invariant`

⟶ checks assertion holds (even if not inductive)`Assume`

⟶ checks assertion holds (even if not subject to proof)`Loop_Variant`

⟶ checks variant decreases wrt previous iteration

### Activating Ghost Code¶

Need to activate ghost code in executable

Ghost code, like assertions, is deactivated by default

- Use
`-gnata`

to activate globally - Use pragma
`Assertion_Policy (Ghost => Check)`

to activate locally

- Use
Inconsistent combinations will be rejected by GNAT

- Ignored ghost entity in activated assertion
- Ignored ghost assignment to activated ghost variable

## Test for Proof¶

### Overflow Checking Mode¶

Problem: ignore overflow checks in assertions/contracts

- Only applies to signed integer arithmetic
- Does not apply inside an expression function returning an integer

Solution: use unbounded arithmetic in assertions/contracts

- Will use 64bits signed arithmetic when sufficient
- Otherwise use a run-time library for unbounded arithmetic

Two ways to activate unbounded arithmetic

- Use
`-gnato13`

compiler switch - Use pragma
`Overflow_Mode`

with arguments`(General => Strict, Assertions => Eliminated)`

in configuration pragma file

- Use

## Test alongside Proof¶

### Checking Proof Assumptions¶

Need to check dynamically the assumptions done in proof

- Postcondition of tested subprogram called in proved subprogram
- Precondition of proved subprogram called in tested subprogram

Other assumptions beyond pre- and postconditions

- Global variables read and written by tested subprogram
- Non-aliasing of inputs and outputs of proved subprogram
- No run-time errors in tested subprogram

GNATprove can list assumptions used in proof

- Switch
`--assumptions`

adds info in`gnatprove.out`

file

- Switch
See "Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification"

### Rules for Defining the Boundary¶

`SPARK_Mode`

defines a simple boundary test vs. proof- Subprograms with
`SPARK_Mode (On)`

should be proved - Subprograms with
`SPARK_Mode (Off)`

should be tested

- Subprograms with
`SPARK_Mode`

can be used at different levels- Project-wise switch in configuration pragma file (with value
`On`

) ⟶ explicit exemptions of units/subprograms in the code - Distinct GNAT project with
`SPARK_Mode (On)`

for proof on subset of units - Explicit
`SPARK_Mode (On)`

on units that should be proved

- Project-wise switch in configuration pragma file (with value
Unproved checks inside proved subprograms are justified

- Use of pragma
`Annotate`

inside the code

- Use of pragma

### Special Compilation Switches¶

Validity checking for reads of uninitialized data

- Compilation switch
`-gnatVa`

enables validity checking - pragma
`Initialize_Scalars`

uses invalid default values - Compilation switch
`-gnateV`

enables validity checking for composite types (records, arrays) ⟶ extra checks to detect violation of SPARK stronger data initialization policy

- Compilation switch
Non-aliasing checks for parameters

- Compilation switch
`-gnateA`

enables non-aliasing checks between parameters - Does not apply to aliasing between parameters and globals

- Compilation switch

## Test as Proof¶

### Feasibility of Exhaustive Testing¶

Exhaustive testing covers all possible input values

Typically possible for numerical computations involving few values

e.g. OK for 32 bits values, not for 64 bits ones

- binary op on 16 bits ⟶ 1 second with 4GHz
- unary op on 32 bits ⟶ 1 second with 4GHz
- binary op on 32 bits ⟶ 2 years with 64 cores at 4GHz

In practice, this can be feasible for trigonometric functions on 32 bits floats

Representative/boundary values may be enough

- Partitioning of the input state in equivalent classes
- Relies on continuous/linear behavior inside a partition

## Test on top of Proof¶

### Combining Unit Proof and Integration Test¶

Unit Proof of AoRTE combined with Integration Test

- Combination used by Altran UK on several projects
- Unit Proof assumes subprogram contracts
- Integration Test verifies subprogram contracts

Unit Proof of Contracts combined with Integration Test

Test exercises the assumptions made in proof

One way to show Property Preservation between Source Code and Executable Object Code from DO-178C/DO-333

- Integration Test performed twice: once with contracts to show they are verified in EOC, once without to show final executable behaves the same

## Test Examples / Pitfalls¶

### Example #1¶

I am stuck with an unproved assertion. My options are:

- switch --level to 4 and --timeout to 360
- open a ticket on GNAT Tracker
- justify the unproved check manually

**Evaluation**: This approach is not correct. Why not, but only after
checking this last option:

- run tests to see if the assertion actually holds

### Example #2¶

The same contracts are useful for test and for proof, so it’s useful to develop them for test initially.

**Evaluation**: This approach is not correct. In fact, proof requires more
contracts that test, as each subprogram is analyzed separately. But these
are a superset of the contracts used for test.

### Example #3¶

Assertions need to be activated explicitly at compilation for getting the corresponding run-time checks.

**Evaluation**: This approach is correct. Use switch `-gnata`

to
activate assertions.

### Example #4¶

When assertions are activated, loop invariants are checked to be inductive on specific executions.

**Evaluation**: This approach is not correct. Loop invariants are checked
dynamically exactly like assertions. The inductive property is not
something that can be tested.

### Example #5¶

Procedure `P`

which is proved calls function `T`

which is tested. To
make sure the assumptions used in the proof of `P`

are verified, we
should check dynamically the precondition of `T`

.

**Evaluation**: This approach is not correct. The precondition is proved
at the call site of `T`

in `P`

. But we should check dynamically the
postcondition of `T`

.

### Example #6¶

Function `T`

which is tested calls procedure `P`

which is proved. To
make sure the assumptions used in the proof of `P`

are verified, we
should check dynamically the precondition of `P`

.

**Evaluation**: This approach is correct. The proof of `P`

depends on
its precondition being satisfied at every call.

### Example #7¶

However procedure `P`

(proved) and function `T`

(tested) call each
other, we can verify the assumptions of proof by checking dynamically all
preconditions and postconditions during tests of `T`

.

**Evaluation**: This approach is not correct. That covers only functional
contracts. There are other assumptions made in proof, related to
initialization, effects and non-aliasing.

### Example #8¶

Proof is superior to test in every aspect.

**Evaluation**: This approach is not correct. Maybe for the aspects
`Pre`

and `Post`

. But not in other aspects of verification:
non-functional verification (memory footprint, execution time), match with
hardware, integration in environment... And testing can even be exhaustive
sometimes!

### Example #9¶

When mixing test and proof at different levels, proof should be done at unit level and test at integration level.

**Evaluation**: This approach is not correct. This is only one possibility
that has been used in practice. The opposite could be envisioned: test
low-level functionalities (e.g. crypto in hardware), and prove correct
integration of low-level functionalities.

### Example #10¶

There are many ways to mix test and proof, and yours may not be in these slides.

**Evaluation**: This approach is correct. YES! (and show me yours)