External Axiomatizations¶
What is it?¶
It is a feature of the SPARK toolset that allows to manually supply a WhyMl translation for the public specification of a library level package that is in SPARK. This feature is still experimental.
Why is it useful?¶
- For features that cannot easily be described using contracts, like transitivity, counting, or summation
- To link functions to the logic world, like trigonometry functions
How does it work?¶
To say that a library package has an external axiomatization, we annotate it using:
pragma Annotate (GNATprove, External_Axiomatization);
These packages should have SPARK_Mode On on their public specification and SPARK_Mode Off on their private part.
The WhyMl translation for the package should be stored in a subdirectory named _theories of the proof directory specified for the project.
What should the translation look like?¶
- For each publicly visible entity E in the package P, it should provide the same elements (types as well as logic and program functions) as the automatic translation, all grouped in one single module named P__e. For example, the module for a function F should provide both a logic function declaration named f__logic and a program function declaration named f.
- For most types, a model module in defined in ada__model.mlw that can be cloned to get most of the required declarations.
- The manual translation may use any type, constant and function that is visible from the Ada package declaration.
- A good way to start an axiomatization file on a package is to launch the toolset on it and copy paste the modules created for each entity of the package. A WhyMl file created by the tool on a package P contains a module for every declaration visible from it, only declarations from P itself should be copied. The generated file usually contains two modules for each entity, one named P__e and one named P__e__axiom. Both should be put together in P__e for the manual translation. The toolset will replace statically known expressions with their value. Beware that they might be architecture dependent.
Example¶
For example, let us consider the following package, stored in a file sum.ads, providing a summation function for slices of arrays of integers:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 | package Sums with SPARK_Mode is
pragma Annotate (GNATprove, External_Axiomatization);
subtype Extended_Index is Integer range 0 .. 2 ** 16;
subtype Index is Integer range 1 .. Extended_Index'Last;
subtype Vector_Element is
Integer range Integer'First / Index'Last .. Integer'Last / Index'Last;
type Vector is array (Index range <>) of Vector_Element;
type Slice_Bounds is
record
Lo : Index;
Hi : Extended_Index;
end record;
function Sum (X : Vector; Bounds : Slice_Bounds) return Integer with
Pre => (Bounds.Lo > Bounds.Hi) or else
(X'First <= Bounds.Lo and Bounds.Hi <= X'Last);
end Sums;
|
We can provide the following Why3 translation for it, that we should store in a file named sum.mlw:
module Sums__extended_index
use import "_gnatprove_standard".Main
use "_gnatprove_standard".Integer
use import "int".Int
type extended_index
function first : int = 0
function last : int = 65536
predicate in_range (x : int) = first <= x /\ x <= last
(* Clone of the model module for discrete types with static bounds *)
clone export "ada__model".Static_Discrete with
type t = extended_index,
function first = first,
function last = last,
predicate in_range = in_range
(* Type for mutable variables of type extended_index *)
type extended_index__ref = { mutable extended_index__content : extended_index }
val extended_index__havoc (x : extended_index__ref) : unit
writes { x }
(* All values of type extended_index are in range *)
predicate dynamic_invariant (expr : int) bool bool bool =
dynamic_property first last expr
(* We know nothing for default initialization of variables of type
extended_index *)
predicate default_initial_assumption int bool = true
end
module Sums__extended_index__rep
use import Sums__extended_index
use import "_gnatprove_standard".Main
(* Projection functions from extended_index to int *)
clone export "ada__model".Rep_Proj_Int with
type t = extended_index,
predicate in_range = in_range
end
module Sums__index
use import "_gnatprove_standard".Main
use "_gnatprove_standard".Integer
use import "int".Int
type index
function first : int = 1
function last : int = 65536
predicate in_range (x : int) = first <= x /\ x <= last
(* Clone of the model module for discrete types with static bounds *)
clone export "ada__model".Static_Discrete with
type t = index,
function first = first,
function last = last,
predicate in_range = in_range
(* Type for mutable variables of type index *)
type index__ref = { mutable index__content : index }
val index__havoc (x : index__ref) : unit
writes { x }
(* All values of type index are in range *)
predicate dynamic_invariant (expr : int) bool bool bool =
dynamic_property first last expr
(* We know nothing for default initialization of variables of type index *)
predicate default_initial_assumption int bool = true
end
module Sums__index__rep
use import Sums__index
use import "_gnatprove_standard".Main
(* Projection functions from index to int *)
clone export "ada__model".Rep_Proj_Int with
type t = index,
predicate in_range = in_range
end
module Sums__vector_element
use import "_gnatprove_standard".Main
use "_gnatprove_standard".Int_Division
use import Standard__integer
use import "int".Int
type vector_element
function first : int = Int_Division.div Standard__integer.first 65536
function last : int = Int_Division.div Standard__integer.last 65536
predicate in_range (x : int) = first <= x /\ x <= last
(* Clone of the model module for discrete types with static bounds *)
clone export "ada__model".Static_Discrete with
type t = vector_element,
function first = first,
function last = last,
predicate in_range = in_range
(* Type for mutable variables of type vector_element *)
type vector_element__ref = { mutable vector_element__content : vector_element }
val vector_element__havoc (x : vector_element__ref) : unit
writes { x }
end
module Sums__vector_element__rep
use import Sums__vector_element
use import "_gnatprove_standard".Main
(* Projection functions from vector_element to int *)
clone export "ada__model".Rep_Proj_Int with
type t = vector_element,
predicate in_range = in_range
end
(* Module for any array type ranging over signed integer types and
containing vector_element *)
module Array__Int__Sums__vector_element
use import "_gnatprove_standard".Main
use import "int".Int
use Sums__vector_element
use Sums__vector_element__rep
function one : int = 1
type component_type = Sums__vector_element.vector_element
(* Clone of the model module for logical arrays containing vector_element
and indexed by mathematical integers *)
clone export "_gnatprove_standard".Array__1 with
type I1.t = int,
predicate I1.le = Int.(<=),
predicate I1.lt = Int.(<),
predicate I1.gt = Int.(>),
function I1.add = Int.(+),
function I1.sub = Int.(-),
function I1.one = one,
type component_type = component_type
(* Primitive equality between arrays *)
function bool_eq (a:map) (af:int) (al:int) (b:map) (bf:int) (bl:int) : bool =
(if af <= al
then al - af = bl - bf
else bf > bl) /\
(forall idx : int. af <= idx <= al ->
(get a idx) = (get b (bf - af + idx)))
(* Clone of the model module for comparison of arrays *)
clone export "ada__model".Array_Int_Rep_Comparison_Axiom with
type component_type = component_type,
function to_rep = Sums__vector_element__rep.to_rep,
type map = map,
type Index.t = int,
predicate Index.le = Int.(<=),
predicate Index.lt = Int.(<),
predicate Index.gt = Int.(>),
function Index.add = Int.(+),
function Index.sub = Int.(-),
function Index.one = one,
function get = get,
function bool_eq = bool_eq
end
module Sums__vector
use import "int".Int
use import "_gnatprove_standard".Main
use "_gnatprove_standard".Integer
use import Standard__integer
use import Sums__index
use import Sums__vector_element
use Array__Int__Sums__vector_element
use Standard__integer__rep
use Sums__vector_element__rep
predicate index_dynamic_property (first : int) (last : int) (x : int) =
first <= x /\ x <= last
(* Clone of the model module for unconstrained arrays *)
type component_type =
Sums__vector_element.vector_element
function id (x : int) : int = x
(* Clone of the model module for unconstrained arrays *)
clone export "ada__model".Unconstr_Array with
type map = Array__Int__Sums__vector_element.map,
function array_bool_eq = Array__Int__Sums__vector_element.bool_eq,
type index_base_type = Standard__integer.integer,
type index_rep_type = int,
function to_rep = Standard__integer__rep.to_rep,
function rep_to_int = id,
predicate in_range_base = Standard__integer.in_range,
predicate index_dynamic_property = index_dynamic_property,
predicate index_rep_le = Int.(<=)
type vector = __t
(* Type for mutable variables of type vector *)
type vector__ref = { mutable vector__content : vector }
val vector__havoc (x : vector__ref) : unit
writes { x }
(* Helper function *)
function _get "inline" (v : vector) (i : int) : int =
Sums__vector_element__rep.to_rep (Array__Int__Sums__vector_element.get (to_array v) i)
(* If vectors are not empty, their bounds are between Index.first and
Index.last *)
predicate dynamic_invariant (expr : vector) bool (skip_bounds : bool) bool =
(if skip_bounds then true
else dynamic_property Sums__index.first Sums__index.last
(first expr) (last expr))
end
module Sums__slice_bounds
use import "int".Int
use import "_gnatprove_standard".Main
use "_gnatprove_standard".Integer
use import Sums__index
use Sums__index__rep
use import Sums__extended_index
use Sums__extended_index__rep
(* Fields for record type *)
type __split_fields =
{ rec__sums__slice_bounds__lo : index; rec__sums__slice_bounds__hi : extended_index }
type __split_fields__ref = { mutable __split_fields__content : __split_fields }
val __split_fields__havoc (x : __split_fields__ref) : unit
writes { x }
(* Record type *)
type slice_bounds =
{ __split_fields : __split_fields }
(* Type for mutable variables of type slice_bounds *)
type slice_bounds__ref = { mutable slice_bounds__content : slice_bounds }
val slice_bounds__havoc (x : slice_bounds__ref) : unit
writes { x }
(* Helper function *)
function _rec__lo "inline" (b : slice_bounds) : int =
Sums__index__rep.to_rep (rec__sums__slice_bounds__lo (__split_fields (b)))
(* Helper function *)
function _rec__hi "inline" (b : slice_bounds) : int =
Sums__extended_index__rep.to_rep (rec__sums__slice_bounds__hi (__split_fields (b)))
(* Condition to be allowed to access Lo *)
predicate sums__slice_bounds__lo__pred (a : slice_bounds) =
true
val rec__sums__slice_bounds__lo_
(a : slice_bounds) :Sums__index.index
requires { sums__slice_bounds__lo__pred a }
ensures { result = a.__split_fields.rec__sums__slice_bounds__lo }
(* Condition to be allowed to access Hi *)
predicate sums__slice_bounds__hi__pred (a : slice_bounds) =
true
val rec__sums__slice_bounds__hi_
(a : slice_bounds) :Sums__extended_index.extended_index
requires { sums__slice_bounds__hi__pred a }
ensures { result = a.__split_fields.rec__sums__slice_bounds__hi }
(* Equality function over slice_bounds *)
function bool_eq (a : slice_bounds) (b : slice_bounds) : bool =
_rec__lo a = _rec__lo b /\ _rec__hi a = _rec__hi b
function dummy : slice_bounds
(* No particular property applies to all values of types slice_bounds *)
predicate dynamic_invariant slice_bounds bool bool bool = true
(* We know nothing for default initialization of variables of slice_bounds *)
predicate default_initial_assumption slice_bounds bool = true
end
module Sums__sum
use import "int".Int
use import "_gnatprove_standard".Main
use "_gnatprove_standard".Integer
use "_gnatprove_standard".Array__1
use import Sums__slice_bounds
use import Sums__index
use Sums__index__rep
use import Standard__integer
use import Sums__extended_index
use Sums__extended_index__rep
use import Sums__vector
(* Logic complete function for sum *)
function sum__logic
(x : vector) (bounds : slice_bounds) :int
(* Helper function *)
function _sum "inline" (x : vector) (bounds : slice_bounds) :int =
sum__logic x bounds
(* Axiom for defining the sum function *)
axiom sum_def:
forall v : vector, b : slice_bounds
[sum__logic v b].
Standard__integer.in_range (sum__logic v b) /\
(* Case of the empty slice *)
(_rec__lo b > _rec__hi b -> _sum v b = 0) /\
(* Case of a non-empty slice *)
(first v <= _rec__lo b <= _rec__hi b <= last v ->
(* If the slice only contains one element *)
(_rec__lo b = _rec__hi b -> _sum v b = _get v (_rec__lo b)) /\
(* Link to smaller slices of the same vector *)
(forall b1 : slice_bounds [sum__logic v b1].
(* Ending at the same index *)
((_rec__hi b1 = _rec__hi b /\ _rec__lo b < _rec__lo b1 <= _rec__hi b) ->
let b2 = {__split_fields =
{rec__sums__slice_bounds__lo = rec__sums__slice_bounds__lo (__split_fields b);
rec__sums__slice_bounds__hi = Sums__extended_index__rep.of_rep ((_rec__lo b1) - 1)}} in
_sum v b = _sum v b1 + _sum v b2) /\
(* Sartind at the same index *)
((_rec__lo b1 = _rec__lo b /\ _rec__lo b <= _rec__hi b1 < _rec__hi b) ->
let b2 = {__split_fields =
{rec__sums__slice_bounds__lo = Sums__index__rep.of_rep ((_rec__hi b1) + 1);
rec__sums__slice_bounds__hi = rec__sums__slice_bounds__hi (__split_fields b)}} in
_sum v b = _sum v b1 + _sum v b2)))
(* Program partial function with a precondition for sum *)
val sum (x : vector) (bounds : slice_bounds) :int
requires { _rec__lo bounds > _rec__hi bounds \/
first x <= _rec__lo bounds /\ _rec__hi bounds <= last x }
ensures { result = sum__logic x bounds }
end