Formal Containers

Formal containers are a new version of Ada containers introduced for the needs of project Hi-Lite. They follow a slightly modified version of the standard API. The purpose of the modifications is to facilitate formal verification of programs using these containers. The semantics of formal containers has been axiomatized in Why and proved in Coq. The technical report is available here.

All source code (Ada, Why and Coq) and tests are in the git repository of project Hi-Lite. To check it out, please use:

git clone http://forge.open-do.org/anonscm/git/hi-lite/hi-lite.git.

The sources are in hi-lite/libs/containers/.

A Library of Containers for Ada

Formal containers have been added to the standard library of the GNAT compiler. Ada sources can be found in the git repository of Hi-Lite in hi-lite/libs/containers/ada.

Axiomatization in Why

The example below is a Why program which applies function f to every element of a list. Its postcondition states that each cursor that formally designated an element e in the list designates f(e) after the call.

(* after map l s, every element in s has been transformed through f *)
let map_f (s : list ref) =
  init :
  let c = ref first !s in
  while not (curs_equal !c no_element) do
    { invariant
     (has_element_(s,c) and has_element_(s@init,c) or c = no_element) and
     (forall cu : cursor. has_element_(left_(s,c),cu) ->
                                       element_(s,cu) = f(element_(s@init,cu))) and
     equal_(right_(s@init,c), right_(s,c))
    }
    replace_element s !c (f(element !s !c));
    c := next !s !c
  done
  { forall cu : cursor. has_element_(s,cu) -> element_(s,cu)=f(element_(s@,cu)) }

To get the complete code of the axiomatization (an axiomatization file and a test file per container) please visit Hi-Lite's git repository in hi-lite/libs/containers/why.

Validation in Coq

Since the axiomatization is quite large, its correctness is an issue. For this reason, each Why file was proved correct using the interactive proof assistant Coq.

We encode lists as a list of pairs cursor/element, which are constrained so that each cursor in a list is unique and different from the special cursor no_element (encoded as 0). In that case, a cursor is valid in a list if-and-only-if it appears in a pair of the list. Valid cursors always designate one and only one element in a given list, the element associated to the cursor in the list. The order of iteration over the list is the classical order.

Each Ada function is modeled in Coq through a corresponding function. For example, in this file, one can see the definition of function replace_element, which returns a list where the element designed by a given cursor is replaced by a given element. We proved in Coq that this function indeed preserves the well-formedness of lists.

The Coq files used for the formal proof of the axiomatization can be found in the git repository of Hi-Lite in hi-lite/libs/containers/coq.

  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org