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)