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)

• 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

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)

• 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

• 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

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

• 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

• 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

• Unproved checks inside proved subprograms are justified

  • Use of pragma Annotate inside the code

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

• Non-aliasing checks for parameters

  • Compilation switch -gnateA enables non-aliasing checks between parameters

  • Does not apply to aliasing between parameters and globals

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)