This repository contains implementations of robot navigation algorithms in Ada/SPARK:
- Vector Field Histogram Plus (VFH+)
- Nearness Diagram Navigation (ND)
- Smooth Nearness Diagram Navigation (SND)
The code is already integrated with the Player/Stage robot programming environment and the integration with ROS is planned.
For details of the algorithms, configuration parameters and references, see the list of Player drivers.
Implementations of VFH+ and ND are based on the latest code from the Player repository. Implementation of SND is based on the code from the author's website, as the code is Player repository seems outdated.
For each algorithm there are
ada folders with the original
code in C/C++, but including our fixes, and the corresponding code in
Only the Ada/SPARK implementation of SND has been fully verified for run-time safety (with the assumption that floating-point operations are exact and do not overflow). The other implementations suffer from poor programming style, which prevented us from proving their run-time safety, and/or rely on code features, such as type invariants, that are not yet supported by SPARK.
The C++ code can be compiled using CMake and the standard procedure
for Player driver plugins. The path to the Player installation needs
to be set in the individual
The code is split into "driver" parts in C++ and full Ada, which integrate the algorithm with the Player, and "algorithm" parts in SPARK, which implement the navigation procedures. The code requires an Ada 2012 compiler and has been developed using GNAT GPL 2013, which can be downloaded from AdaCore.
To build Player plugins use
gprbuild -P driver in the
of the individual algorithms. The path to the Player installation
needs to be set in the
driver.gpr files. The plugins depend on two
assertionsshould be set to
disabledepending on whether the run-time checks should be generated by the Ada compiler,
numericsshould be set to
nativeto use mathematic functions from the Ada standard library or
libcto use faster, but less accurate functions from the C standard library.
For example, to build the SND driver with assertions enabled and the
native Ada mathematic functions, use
gprbuild -P driver -Xassertions=enabled -Xnumerics=native in the
To statically verify the "algorithm" code for run-time safety you need a GNATProve with the support for formal containers and formal numerics libraries. For details of the installation process see the formal numerics package README file.
Once you are comfortable with the tools, you can:
check if the code is in the SPARK subset of Ada:
gnatprove -P algorithm --mode=checkand inspect the
do data-flow analysis:
gnatprove -P algorithm --mode=flow,
gnatprove -P algorithm --mode=prove --proof=then_split.
To benchmark the Ada/SPARK code you can use a
goto utility. Once the
robot reaches the goal location, the drivers prints a message with the
number of iterations and the CPU time consumed by the algorithm.
To ease the benchmarking, the driver will shutdown the Player process
after reaching the goal location. This behaviour can be disabled by
exit(0) call in the C++ driver code.